TLA-Verus: LLM agents prove temporal properties of TLA+ specs

This NeurIPS'26 workshop paper takes TLA+ specs from GitHub, translates them into Verus, and has LLM agents prove the safety and liveness properties in the specs.The motivationThe paper aims to address two problems it raises with TLA+. First, nothing ties the spec to the code, so they drift apart. And second, it claims that proof support is thin: TLC only checks small configurations, and TLAPS is weak on liveness.They abandon pursuing the first weakness they raise at the onset of the paper. Closing it needs a proof that the generated Rust code (which it turns out TLA-Verus doesn't produce anyway) refines the spec, so they list this as future work. It gets worse though. There is no refinement proof between the TLA+ spec and the Verus spec either. Nothing establishes that the translated Verus spec means what the original meant. (Trace validation, meanwhile, is a viable way of tying TLA+ to implementation code, and has been getting a lot of attention recently.)They dedicate the paper to…