The paper reports that all 1,325 theorems from the VeriContest benchmark—comprising 1,007 competitive‑programming problems in Rust with Verus specifications—were successfully proved using Rust‑Prover, a Lean 4‑based verifier. The authors translated each Verus specification and Rust program into Lean, then used Lean’s kernel to confirm the proofs, achieving a 70% first‑iteration success rate and completing 1,259 proofs in under 32 hours on Claude Opus 5.5. The translated Lean programs matched the original Rust outputs on 21,413 benchmark test cases, and the study also compared performance across multiple large‑language‑model settings, noting that higher reasoning effort increased cost without improving proof counts.
By Traian Serbanuta, Jun Xu, Andrei Stefanescu, Cosmin Radoi
The paper introduces agentic verified optimization, where an AI agent produces a faster implementation of a program along with a machine‑checked proof that it is behaviorally equivalent to the original. The authors implement this in Lean 4, creating Aqueduct to migrate C, C++, Go, and Rust code into Lean and validate the ports via differential testing. On 189 reference functions, agents achieved 156 faster, proved rewrites, and on 17 migrated applications, 92 rewrites improved 47 of 51 scenarios, demonstrating the feasibility of verified optimization for real‑world software.
By Zhe Ye, Udaya Ghai, Zhizhen Qin, Dawn Song, Soonho Kong
arXiv:2602. 09464v2 Announce Type: replace-cross Abstract: Vericoding refers to the generation of formally verified code from rigorous specifications.
By Haoyu Zhao, Ziran Yang, Jiawei Li, Deyuan He, Zenan Li, Chi Jin, Venugopal V. Veeravalli, Aarti Gupta, Sanjeev Arora
arXiv:2603. 18334v2 Announce Type: replace-cross Abstract: As Large Language Models (LLMs) increasingly assist secure software development, their ability to meet the rigorous demands of Rust program verification remains unclear.
By Zichen Xie, Wenxi Wang
arXiv:2608. 09277v1 Announce Type: new Abstract: Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promising software that is correct by construction.
By Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li, Kaiyu Yang
arXiv:2603. 19329v3 Announce Type: replace-cross Abstract: Large language models (LLMs) can generate plausible code but offer limited guarantees of correctness.
By Zenan Li, Ziran Yang, Deyuan He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, Chi Jin
arXiv:2610.17331v1 Announce Type: new
Abstract: General-purpose coding agents use standard shell and file interactions, yet formal theorem-proving agents often rely on specialized, ad-hoc tooling. Th...
By Tomas Ortega, Simon Park, Ayush Khaitan, Liam Fowl, Alex Kontorovich, Sanjeev Arora
arXiv:2607. 17352v1 Announce Type: new Abstract: Designing effective Lean proof agents is a central challenge in formal mathematical reasoning.
By Yuqing Li, Zeguan Wu, Yu Gan, Junyu Liu
The paper introduces RefactorProof, a benchmark that tests whether proofs generated for code remain valid after program refactoring that preserves behavior. Using 458 Lean-certified variants derived from 185 VERINA tasks, the study finds that structural refactorings expose brittleness in proofs, with task-normalized structural PSR ranging from 4.3% for supplied references to 13.3–26.8% for specialized provers. Despite higher failure rates, specialized prover proofs (DeepSeek-Prover-V2-7B, Goedel-Prover-V2-32B, Goedel-Prover-V2-8B) show significantly higher unchanged-proof survival compared to reference artifacts, and many failures can be repaired with minimal edits.
By Aravind Mandiga, Guoming Li
arXiv:2609.21190v1 Announce Type: cross
Abstract: Ensuring the correctness of LLM-generated code is a core challenge for modern software engineering. Benchmarks for agentic code generation check corr...
By George Ma, Benjamin Mikek, Haoyu Li, Ferhat Erata, Yuhao Zhang, Zeren Shui, Behrooz Omidvar Tehrani, Jun Huan, Murali Krishna Ramanathan, Somayeh Sojoudi, Hao Zhou, Anoop Deoras
arXiv:2608. 13522v1 Announce Type: cross Abstract: AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code.
By Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song
arXiv:2607. 06341v1 Announce Type: cross Abstract: Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort.
By Shuangxiang Kan, Shuanglong Kan, Sebastian Ertel