I kinda want to learn formal verification, but there are too many questions about actually implementing it in software. This implementation gap is one of them. Posting them here in case anyone has...
I kinda want to learn formal verification, but there are too many questions about actually implementing it in software. This implementation gap is one of them.
Posting them here in case anyone has answers:
How do you ensure that implementation matches the specification. I tried TLA+ modeling in a project, it caught a bug, which I read as sound and fixed it. That fix caused production outage, turns out I was modeling the concurrency wrong in TLA+ (because it is really hard to model it correctly and in performant way - if I coded to my specs the software would be serving a single user at a time instead of thousands).
From my recent search the best approaches would be:
Rocq of Rust (formerly Coq of Rust) from the Cryptocurrency world do this by converting your actual Rust code into Rocq code, then you write your proof in Rocq itself
Lean 4 is an actual programming language. I heard the Lean 4 compiler is self hosting, but I don't know how performant Lean 4 program could be and the ecosystem. Would you want to write an entire microservice in Lean? or does Lean has a good FFI so that critical sections can be written in Lean and wrapped in other languages (similar to how the Python community use Cython or PyO3)
What do you even prove for in a normal web application? For example, what proofs do you write to ensure that Tildes is bug-free?
What classes of software testing could Formal Verification can replaces? For example, assuming that the code 100% matches specification, do I still need unit testing if I can express all the test cases as theorem?
Despite the paper’s famously accessible style, we’ve found bugs in every Raft implementation we’ve tested, including HashiCorp Raft, Aeron Cluster, OpenRaft, and MicroRaft — despite the investment in formal methods, careful code review, unit testing, and years of testing in production. The bugs we found manifest as violations of Raft’s main invariant (called state machine safety in the paper, commonly referred to elsewhere as total order delivery). If you’re using a Raft implementation, you might want to check it for bugs.
We’ve sent bug reports upstream. This isn’t intended as a critique of Raft, its authors, its implementers, or any particular implementation. Raft implementations, even with a formal specification and a detailed implementation guide, are not easy to write.
Rather, this is a story about correctness in distributed systems — the inevitability of bugs, the inadequacy of any single approach, and the high cost of learned helplessness.
[...]
In all cases, network partitions and turbulence were sufficient to surface examples of divergence (i.e. no node kill/restart required, or disk corruption, or other faults)
[...]
If there is a single lesson to be learned here, it’s that formal methods alone cannot ensure that software works, because the formal specification still needs to be implemented, and even if you have mechanized verification, you’re verifying the model and not the implementation itself.
We believe formal methods are useful and necessary — they can confirm the basic soundness of a design, and provide a map that saves engineers from many of the errors that can arise in the implementation of a complex system.
But as these bugs show, errors continue to arise when translating the formal specification to production code. In the course of our work with various Raft implementations, we identified a number of assumptions in the Raft paper that remain implicit. An implementer who misses any of these details is likely to run into trouble.
I kinda want to learn formal verification, but there are too many questions about actually implementing it in software. This implementation gap is one of them.
Posting them here in case anyone has answers:
From the article:
[...]
[...]