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.
Authority
6 entries exploring this thread.
Why I built Auths
I built Auths to separate identity from authority and make exact, bounded authorization portable across systems that will inevitably change.
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.
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.