Rainbow, a theorem prover for business-critical algorithms

Note added 15 October 2026: Rainbow’s v1.0.0 release documents this more exactly than the entry does. Each of the 222 algorithms has kernel-checked theorems about its decision step; for most, the theorems check worked instances, and 48 of the 415 proof modules prove a statement for all inputs. Classical guarantees are claimed only where a theorem states them. See doc/claims.md in the repository. The entry below stands as it was written.

Note added 16 October 2026: the trusted kernel has grown since this was written. At Rainbow v1.5.3 (2 November 2026) it is 1,706 lines in the same four files; the 1,200 below is v1.0.0’s. A release test still pins its length.

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 has graduated from a lab proof of concept into an open-source core with a commercial layer on top. The full product page covers capability, architecture, benchmarks and how to get involved.