Code conformance yet again, this time with SMT

[Igor Konnov]

Hi,

I've realized that some of you on this list may be not reading social
networks. So I've decided to send a link to my blogpost here. For
those who have seen it already on LinkedIn/X, apologizing for
inconvenience.

https://protocols-made-fun.com/tlaplus/2025/12/15/tftp-symbolic-testing.html

The most important highlights:

- Closing the gap between TLA+ specifications and the implementations
with interactive symbolic testing. The implementation gets inputs from
the specification, and the specification gets the outputs back into
the model checker's SMT context. Not a new idea, but it's the first
time it works for TLA+.
- Bootstrapping a test harness with Claude, including several Docker
containers, a Docker network, C&C script to control the test clients
in the containers and communicate with the SUT over UDP.
- Generating sequence charts with Claude from the real logs that are
produced by the harness.
- Adding adversarial behavior to the clients in the TLA+ spec.
- Testing several implementations of the TFTP network protocol as a
case study, plenty of bugs in my TLA+ specification, and a few
unexpected findings in the implementations.
- A new lightweight API for Apalache, to script symbolic execution of
TLA+ specs any way you want.

Best regards,
Igor