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 replays a bundle’s declarations and proof terms through kernel/add-declaration, 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 tactic returns the state it was given, unchanged, with a :failure map. The test proof-states-are-immutable-and-failure-is-nondestructive checks this.
• The kernel keeps no global state: “No mutable registry is consulted or changed.” An environment goes in and a new one comes out.

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,364 lines, and the release test v1_release_test fails if their length changes. 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, 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). 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”. All but eight of the corpus’s theorems report axiom-free. 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 in Rainbow Pro.