The secret to model checking is to understand that you're building and verifying a specification in code. It works best if specifications are built function by function. For each function, I'll build "shadow functions" that simplify any functions it calls with a range of potential non-deterministic behavior that matches that function's contract. In this way, formal specifications can be built from the ground up by first verifying a lower-level function and then replacing it with a shadow function that mimics its behavior in a non-deterministic but SMT solver friendly way.
There are things that model checking doesn't do well. Anything with recursion or looping that can't be easily broken down will not perform well with a model checker. While algorithms like balanced binary trees or sorting can be broken down in a way that can be model checked, other algorithms may require the sort of induction one gets with constructive proofs to sufficiently verify. There is an art to this which will lead to style changes in C and a slightly different way of building up functions from pieces that can be trivially model checked. Honestly, that's not a bad thing.
For the parts that can't be easily model checked, I'm working on a C parser library that can be formally verified, which will import C directly into Coq or Lean. I consider that the "last mile" before formal methods in firmware and system software is to the point that it's generally available.
Is there a book or article that talks more about this? I.e. how to write code in a way that is more amenable to model-checking (bounded or otherwise)?
For system programming or firmware, it's incredibly useful. I've used this tool in conjunction with threat modeling and attack surface minimization to significantly improve the safety and security of software written in C. At this point, I would not consider working on any C project that did not make use of this tool.
Embedded, automotive, space use it regularly.
I've setup cbmc and goto-analyzer for string searching algos here https://github.com/rurban/smart and really found some bugs in old published algos.
Two projects sought to mitigate these issues by going in different directions. One was a compiler backend that aimed to be easy to learn with well-specified IL. The other aimed to formalize LLVM’s IL.
https://github.com/AliveToolkit/alive2
There have also been typed, assembly languages to support verification from groups like FLINT. One can also compile language-specific analysis with a certified to LLVM IL compiler. Integrating pieces from different languages can have risks. That (IIRC) is being mitigated by people doing secure, abstract compilation.
There is a fork of CBMC called ESBMC that does this and many other changes: https://ssvlab.github.io/esbmc/documentation.html
Removed due to my misunderstanding:
~~I don't think Kani counts as a "formal" verification tool, emphasis on "formal", but it is a verification tool for rust code and is powered by CBMC.~~
Seems like I misread the documentation...
~~What I was implying is that Kani just can't figure out all of the paths;~~ ~~Consider this example from Kani documentation [1]:~~
fn estimate_size(x: u32) -> u32 {
if x < 256 {
if x < 128 {
return 1;
} else {
return 3;
}
} else if x < 1024 {
if x > 1022 {
panic!("Oh no, a failing corner case!");
} else {
return 5;
}
} else {
if x < 2048 {
return 7;
} else {
return 9;
}
}
}
https://model-checking.github.io/kani/tutorial-first-steps.h...
CBMC is a formal verification tool which tries to prove that there aren't any bugs (where "bugs" means things like UB).