Research

The documents the implementation is held to.

Papers, the evidence behind them, and the sheets that map the system. Everything here is checkable against the repository, and where a claim rests on a proof the proof is published with it.

65Kani harnesses
7functions extracted to Lean
5generated Lean files, hashed
0sorry allowed in CI

Axiom policy: propext, Classical.choice, Quot.sound. A sorry surfaces as sorryAx and fails the build.

Systems monograph · PDF · 15 pages The architecture of forgetting. A privacy microkernel, drawn from the metal up. Runs from RAM, no authority by default, proves itself. The argument in thirteen plates, none of them decoration: each is a mechanism you can check. Open Verification paper · DOCX What is proven, and how. The verification programme behind the kernel: functions lowered from real Rust MIR by Charon and translated to Lean by Aeneas, then proven on the extracted definition; Kani harnesses over the rest; a fixed axiom policy with sorry forbidden in CI. Open Evidence file · JSON The evidence, as data. The machine-readable record the verification paper is held to: the allowed axioms, the extracted functions with the SHA-256 of every generated Lean file, the Kani harness count, the toolchains. Diff it against the repository. Open Reference sheet · PDF · 1 page The system, on one page. The subsystems and the boundaries between them on a single sheet: what the kernel keeps, what the capsules own, and where the trusted path runs. Open

Under work

More is being written.

The shield circuit, the STARK attestation stack and the capsule model each have a paper in progress. They appear here when they can be checked, not before.

The repositories Verify the release