Backbuild Prove

Backbuild Prove is formal verification that lives in your source code. You write proof annotations in ordinary documentation comments, a higher-order-logic (HOL) kernel verifies them mathematically, an independent Lean 4 engine cross-checks the result, and you ship with a cryptographically signed certificate that anyone can verify for free.

This overview explains what Prove is, who it is for, how it differs from testing and linting, and exactly what you are trusting when the kernel says a proof holds. By the end you will know whether Prove fits your work and which guide to read next.

What Backbuild Prove Is

Most tools that check code sample it: a test runs the cases you thought of, a linter matches patterns it was taught. Backbuild Prove instead establishes that a property holds for every input and state a function can reach, by constructing a mathematical proof and checking it against a small, fixed logical foundation. A proof does not find bugs the way a test does; it rules out an entire class of bug.

You express what a function guarantees (its preconditions, postconditions, and the reasoning that connects them) as a prove:pf2 annotation inside a documentation comment, directly above the code. Nothing about your program changes: annotations live in comments and add zero runtime overhead. When you verify, the kernel reads the annotation, reads a formal translation of the code, and confirms the proof is consistent with both. If the proof claims something the code does not do, the kernel rejects it.

Prove has two faces that share one kernel:

• Per-function proofs. Prove one function at a time against its own contract: this parser never reads out of bounds, this division is always defined, this sort returns a sorted list. Start on Writing pf2 Annotations.
• Project-wide governance proofs. Prove a property holds at every matching call site across the whole codebase: every handler checks authorization, every tenant query is scoped, every write is audit-logged. See Governance Proofs.

Who It Is For

Proofs That Keep AI Agents Honest

Backbuild Prove was designed for a world where AI coding agents write much of the code. An agent can draft the proof annotation just as it drafts the function, then iterate against the kernel until it verifies. What makes an AI-drafted proof trustworthy is that the checker, not the model, is the source of truth: an agent cannot talk its way past a mathematical proof obligation the way it can talk its way past a code review.

1. The agent writes the annotation. It learns the format from examples and documentation during normal tool use. No special training or fine-tuning is required.
2. The kernel verifies. Every step must follow from the foundation and previously proven theorems. A false step is rejected.
3. The editor shows the diagnostic. A failed proof is a red squiggle with a precise message, exactly like a type error.
4. The agent self-corrects. It reads the message and fixes the code or the proof, with no human follow-up prompt. The loop closes only when the property actually holds.

What You Are Trusting

The first question a serious reviewer asks is: if the prover says "proved," what exactly am I trusting? The honest answer is a small, auditable foundation, and a second engine that re-checks the result.

• A small trusted core. The kernel rests on a handful of foundational axioms and a fixed set of primitive inference rules. Every theorem in the standard library and every proof you write is reduced to those primitives. There is no path that accepts a result without deriving it. This small core is the entire trusted computing base for primary verification.
• An independent second checker. After the HOL kernel accepts a proof, it is exported to Lean 4, a proof assistant built by a different team on different mathematical foundations, which re-derives the result on its own. For a false result to survive, both engines would need compatible bugs that accept the same invalid proof. Lean 4 cross-check is included on Business and Enterprise plans.
• Explicit assumptions at the edges. Where code cannot be translated (foreign functions, inline assembly, hardware, third-party libraries), you record the boundary as a cited assumption the reader can see, rather than pretending it was proved. What is assumed versus proved is always visible.

Two Ways to Write a Proof

Prove accepts two input formats, and the same kernel verifies both:

• pf2, a dense, machine-first notation the kernel consumes directly. Best for engineers annotating functions. See Writing pf2 Annotations.
• Modified amsthm, the natural mathematical style of published papers plus about five extra macros, which translates deterministically to pf2. Best for mathematicians. See the Modified amsthm Format.

The Verification Workflow

However you write proofs, they flow through four stages:

1. Annotate. Write a prove:pf2 annotation in a documentation comment: the contract and a proof that the implementation satisfies it.
2. Verify. Your editor or the CLI sends the annotation to the kernel, which checks every step. Unchanged annotations return from cache instantly, so re-verification is cheap.
3. Review. Results appear inline in the editor and in CLI output: verified, failed (with a precise reason), cached, or skipped. You or an agent fix any failure.
4. Certify. When proofs pass, publish a signed certificate that anyone can verify, with no Backbuild account, at a public URL.

Where to Go Next