PROOF ASSISTANT · RUST
Kamo
An experimental Cartesian cubical proof-assistant kernel written in Rust.
What it explores
Kamo is a small kernel built around safe indexed arenas and explicit S-expressions. Its examples include checked definitions of equivalences, ua, identity and Boolean-negation equivalences, and a full univalence theorem.
Implementation
The checker deliberately keeps its trusted surface understandable: definitions are ordered and explicit, universe levels are explicit, and the public Rust API exposes checked programs rather than unchecked evaluator entry points. Resource limits bound parsing, evaluation, arena nodes, face solving, and quotation.
Why I find it interesting
Kamo sits exactly where several of my interests meet: programming-language implementation, proof assistants, cubical type theory, and the practical engineering needed to turn mathematical reduction rules into a usable kernel.