AI needs proof. Proof needs AI.
How LLMs can make formal verification economical, formal verification can make generated software accountable, and PDD keeps the human responsible for the claim.
Formal Methods
4 entries exploring this thread.
What does a green build prove?
How Auths and auths-proof led to Proof-Driven Development and Proofbound, an assurance compiler that keeps tests, proofs, bounds, and assumptions distinct.
What is PDD?
Proof-Driven Development makes claims the unit of software work, then promotes them from an honest CLI ledger to bounded checks, Lean theorems, and shipping-code or artifact bindings.
A proof should break when the program changes
How Auths Proof translates its production Rust authority kernel through Charon and Aeneas, refines it against a readable Lean specification, and makes semantic drift fail CI.