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.
Writing
Ideas worth
exposing.
Technical notes, long arguments, and unfinished ideas shared before certainty sands away their useful edges.
Featured
All writing
13 entriesWhat 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.
AI is producing gara-ware
Japanese feature phones evolved into many local variants. AI is creating the same conditions for software, unless applications give way to malleable tools.
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.
Why I built Auths
I built Auths to separate identity from authority and make exact, bounded authorization portable across systems that will inevitably change.
What Japanese taught me about what people leave unsaid
Japanese taught me that understanding depends not only on what a sentence contains, but on what two people can safely omit.
I learned Japanese by starting with kanji
Seventeen years of Japanese began with a year of kanji, followed by grammar dictionaries, half-understood podcasts, and comedy with captions.
A dependency update can change what your program is allowed to do
A capsec diff of two published Rust crate versions shows why dependency review should include newly reachable filesystem, network, process, and FFI behavior.
A function signature should say what the function can do
How capsec makes filesystem and network authority visible in Rust types, what the compiler rejects, and where audit must take over.
Authority should only get smaller
Why auths-proof separates identity evidence, delegated authority, and application execution behind one offline verification contract.
The repository rejects reverse dependencies
How auths-proof turns layer direction, offline verification, deterministic CBOR, and protocol bounds into executable repository checks.
One authority model, many identity and transport systems
How auths-proof admits KERI, raw keys, P-256, Iroh, HTTPS, and other systems without letting them redefine permission.