Why it works this way

The README starts from one problem: “Most ‘verified’ claims fail in the same place: a theorem about a model, a program that allegedly implements the model, and nothing checking the link. Rainbow was built to be exact about that gap rather than to hide it.”

Proofs are data

“A proof is a value. You can store it, diff it, hash it, ship it and re-check it, and a verified result becomes a building block for the next one.” (README)

• lein reproduce rebuilds a content-addressed checkpoint from source and compares hashes.
• lein verify --bundle installs the named base modules, checks the resulting environment id, then replays the bundle’s declarations and proof terms through kernel/add-declaration (inductive blocks through add-inductive-block), so the kernel alone checks a proof made elsewhere. See Proof bundles.
• The dependency graph of the corpus “can be read, checked and installed without running anything first” (doc/modules.md).
• rainbow.repl/declare-theorem “interprets a quoted proof program without host evaluation”.
• A failed primitive tactic returns the state it was given, unchanged, with a :failure map. The test proof-states-are-immutable-and-failure-is-nondestructive checks this.
• kernel/add-declaration consults or changes no mutable registry: an environment goes in and a new one comes out. The kernel keeps only caches that do not change results, and a reduction budget you can rebind.

Notation and abbreviations are Clojure functions that return vectors, so the elaborator only resolves names.

A small kernel

“A proof checked by Rainbow is exactly as trustworthy as the code that checked it” (doc/trusted-base.md). That code is kernel.clj, term.clj, environment.clj and canonical.clj, 1,712 lines, and the release test v1_release_test fails if their combined length changes. Below it the kernel trusts the Clojure reader and compiler, the JVM, and the JDK’s SHA-256. The kernel has needed fixes. “1.0.0 accepts a proof of False”: it “restarted binder numbering at every nested Pi”, so two different inductive blocks received the same block id, and 1.1.0 repaired it (CHANGELOG). 1.4.2 made two soundness fixes, both about inductive types (CHANGELOG). 1.5.2 fixed a defect by which two different declarations could share one content id, which with the opt-in proof-irrelevance axiom let the kernel accept a proof of falsity (CHANGELOG). 1.5.5 fixed eta contraction, which could capture a variable, so the kernel treated two different functions as equal and accepted an axiom-free proof of forall R : Prop, R (CHANGELOG). Logic is built on top: truth, falsity, conjunction, disjunction, existence and unique existence “are impredicative eliminators into Prop” and need “no new kernel rule or trusted primitive” (rainbow.math.logic.proposition). The trusted base lists what the kernel relies on.

Names are hashes

“Names are navigation aliases, never identity” (rainbow.environment). A declaration’s id is the SHA-256 hash of a canonical encoding of its content (for inductive members, of their block’s normalized spec and their position in it), so renaming changes no id (test aliases-do-not-change-semantic-identity), and ids and normal forms agree across twenty fresh JVMs (test semantic-hashes-and-normal-forms-match-across-twenty-fresh-jvms). Names are pinned separately, by a names id that replay reports and bundles record (Content addressing). doc/bundles.md: “A decoding defect therefore shows up as a refused bundle, never as an accepted wrong one.” The price is SHA-256 itself: a collision “would let two declarations share a name”. See Content addressing.

Tactics are untrusted

rainbow.tactic describes itself as “Untrusted proof-state transformations. Success is always reconstructed by the kernel.” Search, the elaborator, checkpoint loading, the ring normaliser and the module installer sit outside the trusted base too, because “a bug anywhere else produces a rejected proof, never an accepted false one” (doc/trusted-base.md). A proof in the REPL ends with kernel/check on the assembled term, even when every step succeeded.

Axioms are explicit

The README: “A logical principle enters only as an explicit axiom declaration, and the kernel computes each theorem’s axiom profile.” lein verify prints that profile for every theorem. rainbow.math.profile declares excluded middle, propositional extensionality, proof irrelevance, function extensionality and choice as axioms: “Profiles change an environment’s assumptions, never the kernel.” An axiom that is not a declared principle “is reported as unknown and blocks any profile claim”. A principle is recognised only when the axiom’s content id is that principle’s own declaration id, and a name the environment does not know is :unknown, outside every profile (CHANGELOG). The coverage tests assert every covered theorem’s profile: axiom-free except eight. The eight, in set_boundary.clj and set_union.clj, depend on logic/excluded-middle or logic/proposition-extensionality.

Stated scope

A checked proof says the theorem is true. lein verify also says how much it covers: all inputs, a definitional unfolding, or a worked instance about specific values. What “proved” means explains the three, and Maturity levels separates a theorem about a model from a verified program. The open core covers Levels 1 to 3. Levels 4 to 6 are Rainbow Pro’s domain; Pro’s programs currently reach Level 5, and Level 6 is the target.