A probe that has never failed proves nothing
Why executable claims need retained counterexamples, distinct failure states, and a gate that distrusts the confidence of its operator.
Writing
Ideas worth
exposing.
Technical notes, long arguments, and unfinished ideas shared before certainty sands away their useful edges.
Featured
All writing
11 entriesA 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.
A machine-checked map is not a solution
What an honest formal map contributes to an open mathematical problem—and why preserving the red nodes is part of the result.