Coding agents learn reusable proof guidance from verification failures
From Verification Failures to Reusable Guidance for Coding Agents
Software EngineeringArtificial IntelligenceLogic in Computer ScienceProgramming Languages
Summary
It can be hard for coding agents to guarantee that computer programs do what they're supposed to do, and that the instructions they check against match what is really needed. The authors show a way to turn mistakes found during program checking into reusable advice that makes future program verification easier. They test this approach on Python coding tasks and find it helps catch hidden mistakes and confirm program correctness more reliably. Their work points toward smarter coding tools that provide proofs programs meet the right requirements.
What this means in practice
- •For software verification engineers: Use reusable guidance to improve program specification and verification workflows for Python coding tasks with higher accuracy and defect detection.
- •For formal methods tool developers: Incorporate human-guided diagnostic procedures into verification tools to help coding agents build proofs and audits that flag and fix subtle program errors.
Authors
Yuqing Zhai, Xiaohong Chen, Lingming Zhang, Sriram Vishwanath, Grigore Rosu
Abstract
Coding agents need to establish that a program satisfies a specification and that the specification captures the requested behavior. We study how expert diagnosis of verification failures can become reusable guidance for this work. Our approach combines executable language definitions in the K framework with a kit of procedures for constructing specifications, repairing proofs, and auditing their adequacy. A human-guided development campaign on HumanEval, a benchmark of 164 Python programming tasks, achieves a 164/164 success rate with the semantics and the kit, measured by final AI audit Pass verdicts after two targeted repairs. To examine whether auditing detects problems that successful proofs leave unresolved, we construct 12 author-reviewed pairs of clean and defective packages. Every package passes its K proofs, and completed audits identify all defects and accept all clean packages. We then use KleverBench to test specification and proof construction for 31 programs with changed operator meanings. Comparisons with complete acceptance rules and equally long generic advice yield mixed results across two model and budget settings, motivating further work on selecting useful guidance within resource limits. Human-reviewed Optimism proofs establish expected pause reverts for six operations within declared input bounds under London semantics with unbounded gas. We report progress, difficulties, and lessons toward agents that deliver programs with checkable correctness arguments.