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...

</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...

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 :)