Six-layer formal verification of the Kevros Enforcement Kernel.
The public paper documents the verification work behind the Kevros actuation-boundary kernel. The model treats AI output as untrusted input and verifies the deterministic enforcement boundary that decides whether controlled action may proceed.
The verified component is the enforcement boundary, not the model.
The kernel sits between autonomous decision-making and consequential action. It checks authentication, mode state, policy decision, evidence write, release token issuance, and actuation-gate verification. The model can be wrong, adversarial, unavailable, or compromised. The verified boundary still closes to denial when required preconditions fail.
Independent verification methods applied to one kernel.
| TLA+ / TLC | System model checked across 1.94 billion generated states, 171 million distinct states, 12 safety invariants, and 4 liveness properties. |
|---|---|
| Kani / CBMC | Rust implementation checked with 17 bounded model-checking harnesses. |
| Verus / Z3 | Unbounded verification work covering 22 verified obligations across mode, pipeline, and evidence-chain properties. |
| Runtime assertions | Production safety checks map back to the TLA+ property set and fail closed on violation. |
| Golden vectors | Cross-language vectors establish byte-identity between Python and Rust decision outputs. |
| Lean 4 | Machine-checked theorem proving with 20 theorems and zero sorry in a zero-dependency Lean formalization. |
The verification set focuses on safety at the point of action.
Safety properties
Permission before power, fail-closed authentication, fail-closed evidence, evidence before token, token required for actuation, mode-decision consistency, fault latching, boot promotion, bounded boot timeout, deny-zero-actuation, and chain integrity.
Liveness properties
Progress to run under persistent good conditions, run exit under low safety, bounded boot completion, and pipeline return to idle.
What this evidence establishes.
Public and controlled evidence are deliberately separated.
| Public paper | Six-Layer Formal Verification paper |
|---|---|
| Public repository | taskhawk-systems/kevros-formal-verification |
| Machine-readable record | kevros-verification-manifest.json in the public verification repository |
| Controlled review | Full deployment evidence, operational runbooks, and customer-specific material are provided through qualified review channels. |