High-assurance compute infrastructure

Projects

These are the named software projects. They serve high-assurance compute infrastructure and Bitcoin infrastructure research, as argued on Philosophy. People who ship with us are on Contributors.

Grok OSS, an open source Grok Build fork that accepts pull requests. It is a userspace harness that will help us bootstrap a provably perfect OS (best we can, despite everything): the most absurdly paranoid and hardened OS that is still computationally efficient. See Grok OSS.

Systems Lean, Lean 4 with linear types for systems programming.

BIP 360 + bip360.org, a proposed Bitcoin soft fork that would add a post-quantum output type (P2MR). That is cryptography meant to remain sound if large quantum computers exist.

libbitcoinpqc + bindings, a post-quantum cryptography library for Bitcoin signatures; bindings by Jeff Bride.

Holy Lean encodes this site's vocabulary and the consistency of the public copy. What it checks is at the end of Philosophy.