Good reference, I had actually starred that on github to refer to later and totally forgot about it.

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

[2] https://sv-comp.sosy-lab.org/2020/

[3] https://cpachecker.sosy-lab.org/