Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)

This artifact packages machine-checked F*/Pulse case studies for proof-oriented programming with AI agents, accompanying the paper "Proofs Promptly: An Experience Report on Proof-Oriented Programming with AI Agents" from ICFP 2026. It includes verified GC and allocator specifications, Pulse implementations,receive-buffer proofs, and verified Pulse stdlib data structures, all runnable through therepository’s Docker-backed make verify workflow with pinned toolchain sources. Artifact reviewers should start at index.html to navigate verified lemmas.