The value of model checking in distributed protocols design | Protocols Made Fun

[giscus[bot]]

The value of model checking in distributed protocols design | Protocols Made Fun

Author: Igor Konnov

https://protocols-made-fun.com/modelchecking/2025/04/08/value.html

[konnov]

You can leave a comment by authorizing giscus to your github, or by interacting with Github discussions directly.

[ericsson49]

Great post, touching multiple important aspects! Really enjoyed it!

[ericsson49]

My maxim is that applying Formal Methods is always beneficial.
Which doesn't mean that it necessarily "adds value", in the sense that the cost can easily outweigh the benefit. It's especially relevant wrt other parties.

One immediate idea is that one can try to reduce the cost of applying F/Ms, i.e. using (or inventing) lightweight Formal Methods.
Model checkers are a nice fit here and perhaps the sweet spot in the industrial setting.
I do agree that it should be combined with testing. And with lots of testing 😄. And one can use Formal Methods to generate tests, which can be very efficient from cost/benefit perspective.

However, I think that starting with a lightweight F/M can be beneficial too. In fact, I prefer to do some formal modeling first (even proving some lemmas), before starting to generate massive amounts of tests. For me, the main benefit here is better understanding of the requirements and figuring out, how to decompose the problem.

Do we need better model checkers?

I think we do need. The world is changing and there arise new problem domains, where cost of bugs can be huge, while applying F/Ms can be relatively straightforward. One example is SNARK circuits, where the most dangerous and easy to introduce bugs are under-constrained bugs. While they are relatively easy to deal with. It's also the case where one cannot be really satisfied even with huge amount of testing.
So, developing specialized model checkers for such domains is one area.

Do we need better generic model checkers? Probably, yes. I think I'd personally prefer custom proof automation. They can be still great to have for general audience.

[ericsson49]

Another question that people in industry are asking: If it takes a year to prove correctness of an industrial-strength protocol with a prover, what do we do after the protocol has been improved by the engineers.

From my experience, efficient proof engineering is an extremely rare skill.
So, I think that industrial application of interactive theorem provers will likely continue to be an outlier in the mid-term perspective.
And perhaps more often a failure than a success.
I doubt LLMs will change that. E.g. if an LLM is able to discharge 60% of verification conditions, there's still 40% left for humans, which is still a lot of effort.

So, I'd rather follow a lighter-weight approach like model checking, perhaps assisted by LLMs (e.g. they can learn from user-provided examples and generate inductive lemmas, or help with converting prose to lemmas/properties). Some modern SMT solvers can output proofs, which can be converted to ITP proofs with some effort.