Model checkers are amazing tools. I've been using one for C development for the past two years, and with the model checker, I feel more confident about code I write in C than I do about code in many other languages.<p>That being said, model checkers find counter-examples. This is not the same as a formal proof. Just because a counter-example cannot be found does not mean that a given property has been proven. It is _extremely_ important to understand that point. Model checking, combined with unit testing, is a formidable tool that should be used whenever possible. But, don't assume that model checking is the same as a proof. The subtle difference does matter, and it can bite you.<p>It is possible to write formal proofs about software, using Calculus of Constructions, Separation Logic, Hoare Logic, etc. However, this is much harder than using a model checker. For 95% of applications, a model checker is good enough.
Interesting coincidence! I just wrote a post on checking Azure firewall equivalence with Z3 two days ago: <a href="https://medium.com/@ahelwer/checking-firewall-equivalence-with-z3-c2efe5051c8f" rel="nofollow">https://medium.com/@ahelwer/checking-firewall-equivalence-wi...</a><p>This post deals with a significantly harder problem, though.
If you're not a fan of lispy languages, Z3 has bindings for .NET, C, C++, Java, OCaml and Python.<p>For example, Python version of the “x + +0 = x” check looks like this:<p><pre><code> from z3 import *
s = SolverFor('QF_FP')
x = FP('x', FPSort(11, 53))
z = fpPlusZero(FPSort(11, 53))
r = RNE()
s.add(Not(fpAdd(r, x, z) == x))
print(s.check())
print(s.model())
</code></pre>
(Except that I hardcoded rounding-mode, because I couldn't figure out how to make an unknown one. :-/)
Does anyone know of any good resources for high-level guidelines on how to incorporate model checking into a typical software development flow? I've only used TLA+ in my own time for some fairly basic modeling of simplified service interactions at work. The team I'm on is soon inheriting a fairly complex codebase that is one of the core backend services at my company. At a high level, it is responsible for kicking off a "state machine" (which spans a few backend services) that ultimately updates a single "item", which is the smallest unit of data we care about. I'd be interested in spending a weekend or two with getting a rudimentary model of it up and running to aid in tech spec writing of new features and perhaps documenting possible bugs in the entire state machine flow. As it stands today, the state machine spans multiple services and is ill defined so I'll be diving into that for documentation purposes regardless, and it seems like creating a codified model simultaneously won't be too much overhead (at the very least, it could be fun).