TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents
cs.LG
Submitted: 2026-10-10
Updated: 2026-10-15
Code: https://github.com/Vanlightly/raft-tlaplus
Sources
- AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement
- A benchmark for vericoding: formally verified program synthesis
- Automated Proof Generation for Rust Code via Self-Evolution
- Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
- Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
- AutoVerus: Automated Proof Generation for Rust Code
- VeruSAGE: A Study of Agent-Based Verification for Rust Systems
- VERINA: Benchmarking Verifiable Code Generation
- RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation
Related papers
- Polynomial-Augmented Neural Networks (PANNs) with Weak Orthogonality Constraints for Enhanced Function and PDE Approximation
- AIRL-S: Unifying Reinforcement Learning and Search-Based Test-Time Scaling via Adversarial Inverse Reinforcement Learning
- Transformers as Bayesian In-Context Experimenters: Smoothness-Adaptive Efficient ATE Estimation
- Convergence issues in Relational Concept Analysis based on AOC-posets
- Beliefs Beyond Posteriors: The Predictive Cost of ELBO Binding
- Understanding Diffusion Models via Ratio-Based Function Approximation with SignReLU Networks