I am interested in proving that some robot controller does not reach any faulty state, which I would define by a set of predicates. I know that there are open-source software tools to achieve that. For instance, I heard of BLAST (Berkeley Lazy Abstraction Software Verification Tool), but are you aware of any other that may be simpler to use and/or more targeted to my particular application?
Have you ever used BLAST or another such tool in one of your project, and do you think that the benefits outweigh the effort needed to deploy such tools?
You might find Frama-C useful.
For evaluations by people who are not Frama-C developers, see these two articles. Some engineers developing safety-critical code (e.g. DO-178B level A) have found formal annotations and analysis based on weakest precondition techniques worth the investment, but traditional tests are very expensive for them. This last link is about Caveat, a closed-source analyzer that Frama-C intends to replace in due time.
Your question makes it sound as if you might perhaps appreciate Frama-C's Aoraï plug-in.
Whether this is all time well spent in your case is probably more a matter of whether you consider learning about these techniques a joy or a chore.