[asxndu]

>... we asked Claude to write a TLA+ specification (spec) for Etcd’s Raft implementation. It passed syntax checks, ran through the TLC model checker, and at first glance looked like a polished formal model.

This is a mistaken use of TLA+!

Leslie Lamport insists that he invented it to be a way of creating "blueprints" for systems.

- You are supposed to go from TLA+ Spec to System (codebase or hardware).

- Not codebase to TLA+ like the author has done.

Otherwise, you may simply model an existing bug properly and the pass all the checks based of its implementation.

He (Leslie Lamport) insists that the value AI can provide is in compiling TLA+ specs to a code base.