A new blog post on: connecting a TLA+ specification to real protocol code using Apalache + Z3, generating tests symbolically and executing them interactively against multiple TFTP implementations. Bootstrapping the test harness with Claude.
protocols-made-fun.com/tlaplus/2025...
What value is your formal spec if it's totally disconnected from the implementation?
Follow the thread...
#tlaplus #testing #smt #protocols
Sunday long read: Specifying and simulating two-phase commit in Lean4.
protocols-made-fun.com/lean/2025/04...
</end-of-thread>
This work was done by @audithare, Jure Kukovec, @robsaltini, @thanh_hai_tran, and myself. We thank @luca_zanolini and @fradamt for fruitful discussions and @ethereumfndn and @ef_esp for the grant under the 2024 Academic Grants Round!
We have introduced several levels of abstractions, to avoid layers of graph problems, hidden inside. We ran Apalache+Z3, Alloy+Kissat, CVC5, for hours and days. It took many iterations, obviously, we found bugs in our specs as well. In the end, accountable safety held through.
Accountable safety was hard to think about, also to automatically reason about, as we found. We put our energy there. Our most direct translation from Python to TLA+ was good enough for finding examples, but showing safety for all combinations was too much for the tools.
We started with the Python specification of 3SF that was recently designed by @luca_zanolini @fradamt @robsaltini @thanh_hai_tran (see the tweet).
x.com/luca_zanoli...
Thinking about distributed algorithms like consensus and their properties is hard. Too many combinations to consider, too easy to give up. Faults make it even worse 🤯 Check our recent report [arxiv.org/abs/2501.07958] for #Ethereum on how model checkers and solvers can help us 🧵
Copilot definitely helps me to quickly write some experimental code in the languages I am not proficient in. It shortens the documentation and google lookups. Sometimes, the produced code is pure garbage, though :)