[eliteraspberrie]

I use Frama-C without the GUI. The annotations do take some effort, but once you get it, it's very intuitive. Start with adding assertions, for example checking that array indices don't go out of bound. Then start with simple function specifications, and improve on them over time.

I wouldn't use it everywhere, but in small, important functions, it's well worth it.

Here's the classic example of reading into a buffer: https://github.com/eliteraspberries/ttyprompt/blob/master/ge... From those few annotations, Frama-C is able to determine that there are no buffer overflows there.