Say what must hold.
Write the behavior you need. Include the good outcome as well as the bad one you want to prevent. A payment system that rejects every payment never exceeds a limit, but it still fails its users.
SPECIFICATION
An independent field guide / 001
Code that does
what you meant.
AI can write the code. You still need to know that it meets the requirement. Proof-driven development makes that requirement explicit, then checks it mathematically.
Start small. State the assumptions. Keep the tests.
01 / Understand the method
Turn “looks right”
into a checkable claim.
A proof establishes that a program or model meets a specification, for all inputs covered by that proof and its assumptions. The hard part starts with deciding what the specification must say.
Try to disprove it.
Give a verifier the code or model and the claim. Ask whether any allowed input makes them disagree. A counterexample tells you where the claim breaks.
VERIFICATION
Keep checking changes.
Run the verifier in continuous integration. Keep tests for the behavior your proof does not cover, such as database calls, browser interactions, and external services.
CONTINUOUS CHECKS
How is a proof different from a test?
A test runs selected examples and checks their results. A formal proof can establish a specified property for every input in a defined model, under explicit assumptions.
Neither tells you that the specification is what your users need. Review the specification, the assumptions, and the boundary between proved and tested behavior. AI can help write these artifacts. A mechanical verifier checks the formal claim.
02 / A small working example
One character.
One broken promise.
The requirement allows a payment that exactly uses the remaining limit. Change ≤ to <, and that valid payment gets rejected.
Set the inputs
Whole units. Spent and limit are nonnegative. Amount is positive.
THE IMPLEMENTATION
allow = spent + amount <= limitFOR THESE INPUTS
The contract holds.
40 + 60 = 100. This payment fits exactly. Both the contract and the implementation allow it.
This interaction checks one example in JavaScript. It does not run a formal prover. Run the Z3 check below to verify the integer model.
Run the actual verifier
Ask Z3 for a counterexample.
The downloadable SMT-LIB files describe the same rule over mathematical integers. Z3 reports unsat for the correct rule: no disagreement exists in this model. For the bug, it reports sat and returns an input that breaks the contract.
TERMINALDownload checker ↓
# After the setup steps linked here
python3 site/examples/check-proof.py
PASS correct rule: unsat
PASS buggy rule: sat
A counterexample is printed below.03 / Choose the right tool
One method.
Different ways to prove it.
Choose the tool for the code and the claim. Our small Z3 example checks a separate model. Other tools can connect proofs more directly to the program you write.
SOLVER / MATHEMATICAL MODELS
Z3
Ask whether a set of logical constraints has a solution. In this guide, a solution is an input where the implementation and contract disagree.
Good starting point: small decision rules. A model proof does not automatically verify the application.
VERIFIER / RUST
Verus
Write specifications and proof annotations alongside Rust code. Verus checks that the supported code satisfies the specified properties.
Good starting point: a Rust function with a precise contract. Review any trusted code outside the proof.
LANGUAGE + PROOF ASSISTANT
Lean
Express programs, mathematical claims, and proofs in one language. Tactics help construct a proof; Lean's kernel checks the resulting proof.
Good starting point: a precise algorithm or mathematical property. Check the definitions and axioms the theorem relies on.
LANGUAGE / CODE + LAWS
Bend 2
Declare application rules in LAWS.bend and provide proofs in PROOF.bend. The checker can reject a change that fails those laws.
Bend is young. Its default checker, compiler, and runtime have documented limits. Proofs cover the encoded laws and semantics.
Bend uses Lean to formalize the kernel behind --verdict. That does not verify the whole toolchain: Bend's documentation says the parser and translation into that kernel are not proved. Read the formalization ↗
04 / Make the trade-off
A proof is useful.
It is not always the next step.
Use proofs for stable, consequential rules. Match the effort to the cost of a mistake, and keep the tests, reviews, and monitoring that cover the rest.
Still exploring the requirement?
Use prototypes and short feedback loops first. A precise proof of a requirement you keep changing can cost more than it saves.
Does a person need to judge it?
Clarity, visual quality, and usefulness need human review and user testing. You can formalize selected interface rules without proving that the experience is good.
Is the change small and low risk?
A focused test or review may give enough confidence. Proof setup and maintenance are real costs; spend that effort where a broken invariant has consequences.
Does the claim cross an unchecked boundary?
Check real integrations with tests and monitor production behavior. A proof that assumes a database, network, or external library behaves correctly does not establish that assumption.
Review the claim before trusting the proof. Missing requirements and false assumptions can leave a correct proof attached to the wrong problem. Tool support, compiler and runtime behavior, and ongoing proof maintenance also limit what a result establishes. This site's Z3 proof covers its mathematical model, not its JavaScript or a production application.
05 / Put the method to work
Small patterns.
Evidence you can rerun.
A companion collection is being prepared for review. It brings the requirement, implementation, check, and verification limits together.
Patterns & examples
Focused rules with an explicit contract, assumptions, and a worked implementation. A deliberately broken version shows whether the check can catch the mistake.
Agent skills
Reusable instructions for keeping the approved requirement intact, running the checker, and reporting exactly what was proved, tested, or left unchecked.
Starter templates
Small projects with pinned tools, local commands, and continuous integration. Start from a complete example before adapting the contract to your own code.
Collection in review.
The public repository link will be added after approval. No collection downloads are released here yet. The introductory Z3 files above remain available.
A pattern's status must come from an actual checker run. A proof applies to its stated claim and assumptions. Agent instructions and setup steps need practical checks too; their prose is not a mathematical proof.
06 / Go to the sources
A short reading list.
A useful next step.
Start with the original material. These projects use different techniques and make different guarantees.
PAPER / 2015
RESEARCH / NOV 2026
Proof Driven Development
Ben Goodspeed's paper describes the workflow using dependently typed programming. The term predates today's coding agents.
Microsoft's PDD Kit demonstration
A research prototype that uses Verus to check agent-written Rust against specifications. The published example examines a web app's login logic.