Phase 3
| Principia Machina: map |
|---|
| Reading the program The move to Lean Status Terminology: the words of both versions |
| Lean itself Lean theorem prover Principia Machina in Lean |
| Version 1 The Principia Machina its specification |
Phase 3: Custos
Goal: the wiki's thin gatekeeper, Custos, built against a rehearsal wiki running the host's software: its page classes, its API module, its jobs run outside the web request, its call into the Calculator with the binary's digest checked, the governor's meter, the derivation class written at landing and the kernel checker, and version 1's landing scenarios replayed with the Calculator as the only calculator.
Done
Open
- The rehearsal wiki on the host's subdomain, the Operator's act, with its accounts.
- The Calculator's residence on the host and the step that places a released binary there.
Next
The first unit: the extension's skeleton, the store seam, the call into the Calculator with the digest check, and a harness that runs without the host.
as of 2026-10-21