Features / Proven decisions
The decisions are mathematics, and the program runs the mathematics.
The rules that decide whether a file opens, whether an approval counts, whether a stopped PC is released, where content may flow, whether the ledger is intact, what may leave the PC and whether a password is released are written in Lean 4 with machine-checked proofs.
zenos-decide, built from the same definitions the proofs are about
the theorems rest only on Lean's standard axioms, and the build fails otherwise
a change that breaks a proof does not ship
How it works
Write, prove, run
Write
Each decision is a Lean function: the facts in, the answer out. Nothing else in ZENOS reimplements it.
Prove
Lean's kernel checks every theorem on every build. A separate check refuses any added axiom.
Run
Every service calls the program built from those definitions and follows its answer. Missing, late or unreadable means no.
- For the network sentinel, it means a cut
What is proved
Six areas, one program
Credit
The idea of proving these decisions in Lean came from Nyxis by Nyx Foundation, which proves the authorization of a web backend. It builds on earlier work such as Amazon's Cedar, whose authorizer is verified in Lean, and the seL4 verified kernel. ZENOS uses none of their code.
Proven, and what is not
Where the proof ends
Checked on every build
- The decisions themselves, over every input
- Properties over any sequence of events, not only single steps
- Signature counting, with signatures modelled as unforgeable
Tested and listed openly
- The cryptography (the model assumes it; a computational proof is out of scope)
- The facts the services read: clearance, enrolled officers, stop state, the clock
- The glue code, the network sensor, the kernel, Python and Lean's compiler