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.
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.
Verification can establish what a machine was permitted to do. It cannot replace openness, interpretation, or an open heart. The essays here move between those worlds without pretending they are the same.
A through-line
Who acted? What could they do? How would we know?
Identity, authority, software behavior, and proof look like separate problems until a system has to answer for itself. My work lives at those seams—and my writing follows the human questions underneath: trust, judgment, institutions, language, and reciprocity.
Recent writing
Notes from the boundary.
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.