Agentic Proof-Oriented Programming — Proof-Oriented Programming in F* documentation

Agentic Proof-Oriented Programming

Agentic Proof-Oriented Programming

AI-based automation of formal proofs has received a lot of attention<br>in the past few years, with lots of promise but few real successes. However,<br>starting in late 2025, with the availability of models such as Claude Opus 4.5 and GPT-5.2 (and beyond),<br>and especially their integration within agentic coding environments such as Claude Code,<br>OpenAI Codex, and GitHub Copilot CLI, the promise of AI automation for proofs has largely<br>become a reality. It is now possible to have agents author hundreds of thousands<br>of lines of programs and proofs, including in F* and Pulse, but also in other<br>proof assistants including Lean, Coq, Verus, Dafny, and others.

For example, in a series of blog posts we have reported on<br>our ability to use AI agents to automatically formalize the classic “CLRS”<br>Introduction to Algorithms<br>textbook in F* and Pulse, in just a few weeks of agentic coding.<br>Beyond just textbook algorithms, we have also been able to use agents to build a<br>formally verified generational garbage collector for OCaml<br>with proofs of correctness comprising more than 100,000 lines of F* and Pulse, authored<br>entirely by agents. The resulting verified, executable C code can be used as a<br>drop-in replacement for the OCaml 4.14.0 garbage collector, and has been tested to work with<br>the OCaml 4.14.0 compiler and runtime system.<br>Going further, we have also been able to use agents to build a verified implementation of<br>the TLS-1.3 protocol,<br>with implementation and proofs again exceeding 100,000 lines of F* and Pulse.<br>The resulting C code interoperates with OpenSSL to negotiate TLS connections and<br>send application traffic.<br>Others have reported similar successes, using agents to formalize proofs of programming<br>language metatheory,<br>parts of verified compilers,<br>or porting C code into Lean with proofs of correctness.

That said, agentic proof-oriented programming is an extremely new paradigm, the agents are evolving<br>rapidly and there are many open questions about how best to structure interactions between humans<br>and agents to achieve the best results. What is clear is that agents can produce software artifacts<br>at a scale which, if not structured correctly, can far exceed the ability of humans to review and validate<br>the results. The promise of proof-oriented programming in this context is that proof checkers like F*<br>can be used to ensures that the software matches a formal specification, but one still has to be able<br>to carefully check that what is proven matches what is intended.

In this part of the book, we offer a few principles and techniques for agentic<br>proof-oriented programming. Thankfully, a lot of what we’ve come to know as good<br>proof-engineering practice is still very much relevant in this new setting. Our<br>main message is that humans need to think carefully about the right abstractions<br>for designing a system so that agents are effective at producing proof-oriented<br>software, and, perhaps more importanly, that humans are able to understand the<br>results.

Contents:

Getting Started

Rubrics, Templates, and Audits

On Abstraction & Rubrics

Rubrics as Templates

Stateful Services

A Verified TLS-1.3 Client and Server

--><br>--><br>-->