Agentic Proving: Claude Code Generates Valid Specifications for 98.8% of Program Verification Problems

arXiv·high signal

Researchers evaluate Claude Code in an agentic proving framework on CLEVER, a Lean 4 benchmark for verifiable code generation. Claude generates valid specifications for 98.8% of problems, with 81.3% also accepted by CLEVER's isomorphism-based scoring. This extends agentic theorem proving beyond pure mathematics into practical program verification, suggesting near-term viability of AI-assisted formal correctness proofs for production software.