TLA-Verus preprint reports machine-checkable temporal proofs using AI agents

Researchers report an AI pipeline that translates TLA+ software specifications into Verus, a verification tool built for Rust, and produces fully machine-checkable proofs of safety and liveness properties. The TLA-Verus preprint addresses verification of distributed systems, including databases, storage systems and coordination protocols. The approach uses both a deterministic translator and an AI agent to convert specifications, then generates the statements that must be proved. The researchers also introduce an evaluation dataset for testing language models on theorem proving in Verus. Their work takes only a first step toward detecting when software implementations diverge from their mathematical specifications.