Cool, I've been meaning to try out Frama-C and other verification tools. Have you tried CBMC or similar tools at all?
1. Try writing C code that's "obviously safe." Gave up on that pretty quickly.
2. Maybe if I make all buffers global, I can verify some basics with a script. Gave up when I learned that "abstract interpretation" already exists, and it's way more advanced than anything I could whip up. (But kept the global buffers for now...)
3. The only example I found for a while was https://github.com/NASA-SW-VnV/ikos, but it needed an old version of Clang, and my laptop didn't have enough memory to build it.
4. Found a couple other examples that were clearly someone's research project.
5. Finally found Frama-C by searching through Fedora packages. And it's exactly what I needed.
There's definitely a learning curve, and it's not always obvious how to get it to do what you want. But I can at least install it, there's a nice GUI, and it's thoroughly documented.
I didn't hear of CBMC until later, but I see there a Fedora package for that too. Should probably take a crack at it!
It is slightly less approachable than Frama-C because it uses separation logic, but it's slightly more approachable because it uses symbolic execution, which allows it to display an actual execution trace that causes the failure. (You can then inspect that and decide whether your code or model is wrong.)
Do you know of a review of the various open source verification tools available for C? The ones I'm aware of: CBMC, Frama-C, VeriFast, ESBMC.
I've found papers like [1] which benchmark various model checkers, but no evaluation of the verification effort required for the various approaches.
Edit: the tutorial for VeriFast does not make it look very usable compared to Frama-C's ACSL language. Their tutorial doesn't explain a bunch of the syntax or why they made certain choices, so it all feels very unergonomic.
Edit 2: The SV-COMP competition on software verification [2] tests a whole bunch of tools, but Frama-C and VeriFast are not among them. Looks like CPAChecker [3] has the best power-to-weight ratio if you're looking for one tool to learn with the most errors caught across all benchmarks.
[1] https://arxiv.org/abs/2003.11689
SV-COMP tends to propose a huge number of relatively simple tasks, which attracts model checkers and static analysers. Frama-C and VeriFast are functional verification tools. You can use them as static analysers, but there's a barrier to entry in terms of minimal required annotations that might not be present for tools designed for static analysis.