TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents

arXiv:2610.14923v1 Announce Type: new Abstract: The TLA+ (temporal logic of actions) formal specification toolkit has seen widespread adoption in modeling modern distributed software systems including databases, storage systems, ledgers and coordination protocols. This popularity is despite its two significant limitations for software verification: Firstly, TLA+ offers no way to detect drift between software implementation and mathematical specification; secondly, TLC and TLAPS cannot provide satisfactory proofs of arbitrary temporal logic properties. We take a step towards addressing these shortcomings by translating TLA+ specifications into Verus, an auto-active verifier built for Rust, via both a deterministic transpiler and an agentic translator. We demonstrate that our LLM-based pipeline is able to generate proof obligations from TLA+ specifications at scale, and to produce fully machine checkable proofs of both safety and liveness properties. Since temporal logic reasoning in Verus is a largely new task for LLMs, our work yields a valuable evaluation dataset, which we use to map out current generation model capabilities in Verus theorem proving.

Related

• Temporal Logic Guided Universal Task Representations for Reinforcement Learning
• Runtime Monitoring of Perception-Based Autonomous Systems via Embedding Temporal Logic
• Mind the Refinement Gap: When Safe High-Level Robot Plans Produce Unsafe Executions

Source: arXiv cs.LG | 2026-10-14