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.
Rust
5 entries exploring this thread.
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.