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

arXiv: https://arxiv.org/abs/2610.14923 · HTML: https://mlsanity.com/paper/2610.14923/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use.
- Builds on 12 of its 37 references that are in the map.
- First posted on arXiv 10 Oct 2026.

## Placed in

- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

## Builds on (most cited first, 12 of 12)

- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [A benchmark for vericoding: formally verified program synthesis](https://mlsanity.com/paper/2509.22908/) (2025)
- [Proving the Coding Interview: A Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2502.05714/) (2025)
- [VeruSAGE: A Study of Agent-Based Verification for Rust Systems](https://mlsanity.com/paper/2512.18436/) (2025)
- [Validating Traces of Distributed Programs Against TLA+ Specifications](https://mlsanity.com/paper/2404.16075/) (2024)
- [Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set](https://mlsanity.com/paper/2602.04910/) (2026)
- [Paxos Made EPR: Decidable Reasoning about Distributed Protocols](https://mlsanity.com/paper/1710.07191/) (2017)
- [Formal Verification of a Distributed Dynamic Reconfiguration Protocol](https://mlsanity.com/paper/2109.11987/) (2021)

## Abstract (arXiv)

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 address the second limitation and take a first step towards the first 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.