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