一句话：经验报告：配备证明助手与 CLI 的 AI Agent 可自动产出数千行机器检验证明代码，把人类专家的工作压缩到给定问题描述与审查规约。
论文关注的问题是：AI 辅助编码的普及带来了更多软件缺陷，那么 AI 辅助的形式验证能否以同等规模减少缺陷？作者以经验报告的形式，记录了他们为 AI Agent 配备命令行接口与证明助手（如 F*/Lean 一类的交互式证明工具），在真实证明工程任务中产出数千行机器检验代码的轶事性经历。任务覆盖三类：为标准库实现经过验证的数据结构、把未验证代码翻译为形式语言并同时推断其规约、以及将既有证明移植并重构到新框架。作者总结了使「智能体式面向证明编程（agentic PoP）」有效或失效的具体技术，并刻画了人类专家的角色——其贡献缩减为提供自然语言的问题描述、审查自动生成的规约、偶尔补充一个关键不变式。结果显示这种人机分工为回路中的人类专家带来可观的杠杆效应：三位专家在两周内完成的案例研究，其手工证明工程成本估计约为半年。
The widespread adoption of AI-assisted coding is directly proportional to an increase in software bugs; can AI-assisted formal verification help reduce bugs at a comparable scale? In this experience report we give an anecdotal account of AI agents, equipped with a CLI and a proof assistant, producing thousands of lines of machine-checked code. We detail our experience across different proof-engineering tasks: implementing verified data structures for a standard library, translating unverified code into a formal language while inferring its specification, and porting and refactoring existing proofs to new frameworks. We present the techniques that made agentic proof-oriented programming (PoP) effective---or ineffective---and characterize the role of the human expert, whose contribution reduces to providing natural-language problem descriptions, reviewing auto-generated specifications, and occasionally supplying a key invariant. Our findings suggest that this division of labor provides substantial leverage to the human expert in the loop: three experts, over the course of two weeks, completed case studies whose manual proof-engineering cost we estimate at roughly half a year.
@article{IoannidisSEPR26,
title = {Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)},
author = {Eleftherios Ioannidis and Nikhil Swamy and Gabriel Ebner and Matthai Philipose and Tahina Ramananandro},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828709}
}