Concepts

The trusted base

A proof checked by Rainbow is as trustworthy as the code that checked it: four files. Tactics, proof search and the mathematics all go through them, so a bug elsewhere gets a proof rejected and cannot get a false one accepted.

The kernel: 1,364 lines

file	lines	role
`src/rainbow/kernel.clj`	1,017	type checking, definitional equality, reduction, natural-number literals and the six native nat operations, inductive types and recursors, universe levels
`src/rainbow/term.clj`	254	the term language: binders, substitution that skips subterms with nothing to change, de Bruijn indices
`src/rainbow/environment.clj`	48	declarations stored by content id, and name resolution
`src/rainbow/canonical.clj`	45	the canonical encoding and the content hash that names every declaration
total	1,364

The functions to read first are infer and check, normalize and definitionally-equal?, add-declaration, add-inductive-block and axioms. The calculus describes what they check. The README calls them 1,364 lines “you can read in an afternoon”.

The size is pinned. A release test, v1_release_test, fails if these four files change length, and CI checks the line count on every push. Version 1.1.0 made checking 24 to 123 times faster, with native natural-number arithmetic pinned to six definitions by content id and a substitution that skips unchanged subterms.

Below the kernel

The kernel trusts the Clojure reader and compiler, the JVM, and the JDK’s SHA-256 for content ids. A collision would let two declarations share a name.

Outside the kernel

Tactics, such as the ring normalisers and the Bool.rec case-split helpers, and elaboration (rainbow.elaborate) produce terms the kernel checks. A wrong tactic yields a rejected term.
Checkpoints: loading one checks each declaration again, so a tampered checkpoint does not replay.
The declaration store, proof bundles and their encodings end in the kernel recomputing ids and checking terms.
The scope lein verify prints comes from rainbow.main, using the kernel’s type inference and the proof term (What “proved” means).

Axioms are explicit

A logical principle, such as a classical one, enters only as an explicit axiom declaration (rainbow.math.profile). kernel/axioms computes each theorem’s axiom profile, lein verify prints it, and the tests assert it for each covered theorem. The profile is empty except for eight named classical theorems.