Rainbow: a theorem prover that treats proofs as data
A Clojure-native dependent-type prover with a tiny trusted kernel, built to prove operations-research algorithms rather than only textbook mathematics.
What it proves
That operations-research algorithms can be machine-checked against a trusted kernel small enough to audit, and that the checked artefact can be reused as composable data, not a one-off transcript.
Built with
Clojure · Dependent types · Content-addressed proof objects
Rainbow began as a proof of concept for one question: can a decision rule that must never fail be verified, not just tested? Tests sample the input space; a proof closes it. For most software the difference is academic. For a rule that allocates staff to projects: one that must never assign someone beyond capacity or break an exclusivity clause: the residual case a test never drew is the entire risk.
What it is
Rainbow is a data-oriented theorem prover written in Clojure. Its trusted base is a dependent-type kernel of about 1,200 lines; everything else, search, tactics, the algorithm catalogue, is untrusted and must emit a proof term the kernel independently checks. That “proof-carrying” split keeps the trusted surface small enough to read and lets an optimised, untrusted engine do the hard search. The kernel is a trusted computing base in the literal sense: it is trusted on inspection, and its own metatheoretic soundness is argued informally rather than being itself machine-checked.
Crucially, Rainbow treats terms, declarations, proofs, failures and provenance as immutable, content-addressed data. A proved reformulation is a reusable object. That makes the economics work: an expensive parametric proof is done once, and a cheap certificate is checked per decision, formal methods that survive in production, not only in a paper.
What it proves today
Its curriculum is the operations-research catalogue behind the book Applied Higher Order Functions: the 222 distinct algorithms distilled from that book’s roughly 480 listings and implemented in the orhof library. It checks signed rationals, finite vectors, Bellman and value-iteration steps and gradient methods natively, compiles truth tables into proof trees, and has machine-checked all 222 catalogued algorithms.
Rainbow is graduating from a lab proof of concept into an open-source product. The full product page covers capability, architecture, benchmarks and how to get involved.
Method disclosure
Partly published.
Kernel, checker, proof formats and semantics are open. The catalogue, the selection graph and the optimised implementations are not.
We publish selectively and say which. Open-source, academic and pro bono work is published in full. Where the mechanism is the commercial asset we publish the result, the evidence grade and the boundary, and state that the mechanism is withheld, and never write around the gap.
Limitations & novelty boundary
Exact about scope: all 222 catalogued OR algorithms are proved, with nothing pending and nothing refuted, but Rainbow still does not claim infinite-horizon or chaotic-relaxation asynchronous convergence, Bellman fixed-point uniqueness, terminating optimal-policy theorems, or a proved correspondence between checked terms and their Clojure implementations. It is open source; the covered set and the remaining gap are published together.