I use Frama-C without the GUI. The annotations do take some effort, but once you get it, it&#x27;s very intuitive. Start with adding assertions, for example checking that array indices don&#x27;t go out of bound. Then start with simple function specifications, and improve on them over time.<p>I wouldn&#x27;t use it everywhere, but in small, important functions, it&#x27;s well worth it.<p>Here&#x27;s the classic example of reading into a buffer: <a href="https:&#x2F;&#x2F;github.com&#x2F;eliteraspberries&#x2F;ttyprompt&#x2F;blob&#x2F;master&#x2F;getline.c" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;eliteraspberries&#x2F;ttyprompt&#x2F;blob&#x2F;master&#x2F;ge...</a> From those few annotations, Frama-C is able to determine that there are no buffer overflows there.