Top Mathematics discussions
NishMath - #verification
|
Igor Konnov@Protocols Made Fun
//
Igor Konnov has successfully completed full proofs of consistency for the two-phase commit (2PC) protocol using the Lean 4 theorem prover, starting from a functional specification. This work builds upon previous efforts in specifying, simulating, and property-based testing 2PC in Lean 4. The entire process, including specification and simulation from prior work, took approximately 45 hours, with the proof writing itself consuming 29 hours. The rapid proof development was attributed to a correct inductive invariant discovered using the Apalache model checker, underscoring the benefits of combining formal specification with interactive theorem proving.
The Lean 4 proofs involved a modular approach, breaking down the verification into functional, propositional, and inductive components. Statistics show that the proofs, propositional and inductive, are about 15 times longer than the system code. Specifically, Functional.lean and System.lean contained 139 lines of code, Propositional.lean had 90, PropositionalProofs.lean comprised 275, and InductiveProofs.lean reached 1077 lines of code. This ratio aligns with the empirical standard in software verification, where proofs typically range from 10 to 20 times the length of the source code. Konnov also mentioned exploring an alternative route: proving equivalence between their specification in Propositional.lean and the Veil specification. The Veil examples repository already contains a version of two-phase commit, albeit slightly different from the TLA+ version and the Lean specification. He suggests that this could be a topic for future work. The consistency of the protocol was specified using TLA+, leveraging its methodology for defining TCConsistent. The Lean 4 code for the two-phase commit protocol can be found on GitHub.
Share:
References :
Classification:
|
Blogs
|