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.
About me
Much of my education has been self-directed: 17 years studying Japanese and 10 years teaching myself software and programming, alongside a background in economics. Those paths shaped an interest in how people express their relation to one another—through markets, language, institutions, and trust.
Recent writing
Notes from the boundary.
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.