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{paperbot3642,
  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}
}