Verified Spec Transpilation with Claude
William Schultz
I ran a small experiment in transpiling TLA+ directly to C++ using Claude, in similar spirit to what SPIN does for model checking efficiency. Validating the state spaces of the original TLA+ against the C++ version allows for a kind of (lightweight) verification harness that the spec semantics were translated correctly. Main limitations of this approach is that this it really only deals with optimizing the "inner interpreter loop" of TLC i.e. it runs single threaded, all data structures are purely in-memory, etc.
Another related, follow-up experiment that would be interesting to run here would be to see if Claude can also auto-convert TLA+ specs directly to a symbolic representation e.g. to SMT-LIB. I imagine we could also do a kind of semi-verified translation in that scenario by asking Claude to write another harness that basically tests for approximate equi-satisfiability between actions in the source TLA+ spec and their generated SMT translation. That is, generate some random, type-correct states for the source TLA+ model, and for each of these, check that, when using these as a starting state/context for an action A, both the TLA+ version of A and the SMT version of A both produce the same set of next states. These next states can be generated by TLC for the TLA+ version and by Z3 for the SMT version. And we just need an appropriate format and logic to convert between the outputs from TLC and Z3 (which Claude should presumably be able to handle fine as part of its validation harness).