Klen
A universal kernel for describing, executing, and formally verifying system safety contracts and state machine invariants in Lean 4.
High-assurance engineering systems require correctness guarantees that traditional unit tests and empirical fuzzing cannot fully provide. Klen investigates the intersection of systems architecture and formal interactive theorem proving, establishing a Lean 4 kernel for mathematically specifying, executing, and verifying system state machines.
System behaviors in Klen are represented as formal state transition systems with inductive safety predicates. Architectural invariants—such as non-blocking progress, session state consistency, and deterministic recovery under partial transport failure—are formulated as theorems and mechanically checked by Lean 4’s proof assistant.
The verified abstractions bridge to real-world software through typed boundary schemas and companion Rust execution harnesses. By enforcing that executable runtime contracts derive directly from formally proven mathematical propositions, Klen guarantees that protocol edge cases and safety violations are caught at proof time rather than in production environments.
Status: active formal verification research harness and proof repository. Kept on local developer workstations.