Cover Image

Agentic Proof Automation: A Case Study

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Xu, Yichen, Odersky, Martin
Format:	Preprint
Published:	2026
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures (Extended Version)
by: Xu, Yichen, et al.
Published: (2025)

Tracking Capabilities for Safer Agents
by: Odersky, Martin, et al.
Published: (2026)

First-Class Refinement Types for Scala
by: Bovel, Matt, et al.
Published: (2026)

LACUNA: Safe Agents as Recursive Program Holes
by: Zhao, Yaoyu, et al.
Published: (2026)

Language-Integrated Recursive Queries (Full Version)
by: Herlihy, Anna, et al.
Published: (2025)

Adaptive Recursive Query Optimization
by: Herlihy, Anna, et al.
Published: (2023)

Automating Equational Proofs in Dirac Notation
by: Xu, Yingte, et al.
Published: (2024)

A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
by: Bayazıt, Barış, et al.
Published: (2025)

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
by: Nagy, Shaan, et al.
Published: (2024)

Refactoring and Equivalence in Rust: Expanding the REM Toolchain with a Novel Approach to Automated Equivalence Proofs
by: Britton, Matthew, et al.
Published: (2026)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
by: Viennot, Jules, et al.
Published: (2025)

A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
by: Xu, Qiyuan, et al.
Published: (2025)

A Natural Formalized Proof Language
by: Xie, Lihan, et al.
Published: (2024)

Agentic Code Optimization via Compiler-LLM Cooperation
by: Mikek, Benjamin, et al.
Published: (2026)

StitchCUDA: An Automated Multi-Agents End-to-End GPU Programing Framework with Rubric-based Agentic Reinforcement Learning
by: Li, Shiyang, et al.
Published: (2026)

Proof Repair across Quotient Type Equivalences
by: Viola, Cosmo, et al.
Published: (2023)

Adaptive Shielding via Parametric Safety Proofs
by: Feng, Yao, et al.
Published: (2025)

Asynchronous Global Protocols, Precisely: Full Proofs
by: Pischke, Kai, et al.
Published: (2025)

Scenario-Based Proofs for Concurrent Objects [Extended Version]
by: Enea, Constantin, et al.
Published: (2023)

Incremental Proof Development in Dafny with Module-Based Induction
by: Ho, Son, et al.
Published: (2024)

Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs
by: Kent, Zachary, et al.
Published: (2025)

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
by: Gross, Jason, et al.
Published: (2023)

Programming Language Case Studies Can Be Deep
by: Bohrer, Rose
Published: (2024)

Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
by: Conoly, Owen, et al.
Published: (2025)

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
by: Paraskevopoulou, Zoe
Published: (2026)

The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version)
by: Schüssele, Frank, et al.
Published: (2025)

Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols
by: Zhang, Tesla, et al.
Published: (2025)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
by: Ravi, Nikil, et al.
Published: (2026)

Symmetric Proofs of Parameterized Programs
by: Cheng, Ruotong, et al.
Published: (2026)

Coinductive Proofs for Temporal Hyperliveness
by: Correnson, Arthur, et al.
Published: (2025)

Unlocking the Power of Environment Assumptions for Unit Proofs
by: Priya, Siddharth, et al.
Published: (2024)

ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
by: Gu, Alex, et al.
Published: (2025)

VeriMind: Agentic LLM for Automated Verilog Generation with a Novel Evaluation Metric
by: Nadimi, Bardia, et al.
Published: (2025)

More Church-Rosser Proofs in BELUGA
by: Momigliano, Alberto, et al.
Published: (2024)

Automated Verification of Soundness of DNN Certifiers
by: Singh, Avaljot, et al.
Published: (2025)

Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity
by: Zhang, Dylan, et al.
Published: (2025)

Automated Expected Cost Analysis for Quantum Programs
by: Moser, Georg, et al.
Published: (2026)

Verification Algorithms for Automated Separation Logic Verifiers
by: Eilers, Marco, et al.
Published: (2024)

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
by: Cao, Jialun, et al.
Published: (2025)

Cyclic Proofs in Hoare Logic and its Reverse
by: Brotherston, James, et al.
Published: (2025)