Open-source theorem proving and formal methods
Rainbow, our theorem prover
We wrote a theorem prover because we needed one: a way to check that the operations-research methods we sell are correct, that does not depend on how careful we were on a given afternoon. Rainbow is written in Clojure, it treats a proof as ordinary data you can store, share and re-check, and the part of it you have to trust is about 1,200 lines long. It has proved all 222 algorithms in our catalogue, and below we say exactly what that does and does not mean.
Open source · EPL-2.0 or GPL-2.0+ · past its v1.0 milestone · Clojure-native trusted kernel
Released capability
What it can do today
These are checked capabilities in the current release, and everything below runs against the trusted kernel. What it cannot do yet is listed further down, at the same length.
The 222 distinct algorithms are those catalogued in the book Applied Higher Order Functions (distilled from its roughly 480 algorithms) and implemented in the orhof library.
Checked natively
- Signed rational arithmetic.
- Finite vectors and their operations.
- Bellman / value-iteration steps.
- Gradient methods.
Tooling
- A truth-table → proof-tree compiler for propositional reasoning.
- Proves all 222 catalogued operations-research algorithms — zero pending, zero refuted.
- Terms, proofs, failures and provenance are all first-class data.
Boundaries
What it does not claim to prove
A proof is only worth something if you know exactly where it stops. These are outside what Rainbow certifies today, and we list them because a reader who found them out on their own would be right to distrust the rest.
Not yet claimed
- Infinite-horizon value-iteration convergence.
- Bellman fixed-point uniqueness.
- A proved correspondence to executing Clojure.
- Broad reconstruction of Mathlib.
Where a result is not proved, the documentation marks it unproved. The kernel will not certify a claim it cannot check. So Rainbow's boundaries are described as boundaries, and nothing softer.
How far a result has travelled
Six levels of proved
A machine-checked theorem and a verified running implementation are different achievements, and most inflated verification claims come from collapsing the two. So Rainbow grades every algorithm on six levels and publishes where each one sits, including the level nothing has reached yet.
| Level | What it means | Ours |
|---|---|---|
| 1 · Research record | Source identified, assumptions and claimed guarantee recorded, complexity classified correctly. | |
| 2 · Human proof | A complete human-readable proof, with hidden assumptions extracted into explicit obligations. | |
| 3 · Machine-checked theorem | The central theorem encoded in Rainbow and accepted by the trusted kernel. Deterministic and reproducible. | 4 |
| 4 · Experimental implementation | Runnable Clojure, connected to the specification. Production correctness not yet established. | 1 |
| 5 · Production-quality implementation | Stable API, error handling, property and adversarial tests, benchmarks, numerical-stability analysis. | 1 |
| 6 · Verified production implementation | A machine-checkable connection between specification and running code. Tests never qualify. | 0 |
Six algorithms currently carry a full manifest, against 222 in the proved catalogue — so the ladder describes a small, deliberately chosen front. Level 6 is empty so far. One Level 5 entry names Level 6 as its target. That is the current frontier of the work. It makes no claim beyond that.
What is open, and what is not
What is open and what is not
The verifier is open. The selection intelligence is not. Here is the line between them, drawn as exactly as we can.
Open
- The trusted kernel and an independent checker.
- Proof and certificate formats, and the formal semantics.
- Conformance tests and the reproducibility harness.
- The verification CLI —
verify,audit,benchmark,reproduce,report. - A selected mathematical corpus and public benchmarks.
Not open
- The full catalogue and the research-selection graph.
- Commercial code-generation orchestration.
- Optimised non-public implementations.
- Customer-specific regulation and policy packs, domain adapters and private data.
The point of the split is that you do not have to trust us. A certificate produced by a proprietary algorithm can be checked by the open verifier without publishing the algorithm or the customer’s data. But checking an output certificate is not the same as proving an arbitrary executable bug-free, and we keep those claims apart.
What remains trusted
Every verification rests on something. Ours rests on the Rainbow kernel, the semantics of the Clojure subset used for generated code, the JVM and its compiler, any native libraries and numerical primitives in the path, and any external solver whose output is not independently re-checked. That list is the honest size of the trust you are extending, and we would rather print it than let “verified” imply it is empty.
Design rationale
Why a proof is data here
Treating a proof as an ordinary, immutable, content-addressed value changes the economics: an expensive proof is done once and checked cheaply forever after.
Immutable and addressable
A proof is a value with a content-addressed identity. It can be stored, shared, versioned and audited like any other data.
Prove once, check often
An expensive parametric proof is produced once. Each subsequent decision carries a certificate the kernel re-checks cheaply.
Composable and reusable
Terms and proofs compose. A verified result becomes a building block for the next one instead of a one-off artefact.
Architecture
How it is built
Rainbow separates the part you must trust from the part that does the work. The engine that searches for a proof can be as clever and as buggy as it likes, because the kernel re-checks everything it proposes.
Trusted kernel · about 1,200 lines
The only thing that decides
Small enough to read and audit. It checks proposed proof terms and certifies them — or refuses. The size of the trusted base is the size of what you must believe. It is a trusted computing base: trusted on inspection, its own metatheoretic soundness argued informally. It is not machine-checked.
Untrusted engine
Proposes, never certifies
The engine may use any strategy to search for a proof. A bug in the engine cannot produce a false certificate, because the kernel checks every term independently.
Worked example
A worked example
Illustrative only, this shows the shape of a proof-carrying check and never the exact library API.
;; Illustrative only: shape of a proof-carrying check.
;; A parametric proof is produced once (expensive); each decision then
;; ships with a certificate the trusted kernel re-checks (cheap).
(theorem gradient-step-decreases-loss
{:assumes [(convex f)
(l-smooth f L)
(step-size a (<= 0 a (/ 1 L)))]
:claims (<= (f (gradient-step x a)) (f x))})
;; The untrusted engine proposes a proof term …
(def proof (engine/prove gradient-step-decreases-loss))
;; … and the 1,200-line trusted kernel is the only thing that decides.
(kernel/check gradient-step-decreases-loss proof)
;; => {:ok true :certificate #rainbow/cert "…content-addressed hash…"}Illustrative pseudocode. Names and return shapes are indicative only.
Roadmap
IdeaWhere Rainbow goes next.
Evidence disclaimer. Everything in this section is intended future work, not released capability. It is deliberately kept separate from what Rainbow checks today. Nothing here should be read as a claim about the current release.
Intended
Deeper decision-theory coverage
The 222-algorithm catalogue is complete. The work now grows the corpus beyond it, towards wider Mathlib and operations-research targets.
Intended
Convergence and uniqueness results
Work towards the convergence and fixed-point results currently listed as boundaries.
Intended
Correspondence to executing code
Investigate a proved correspondence between checked terms and the Clojure that runs them.
Commercial uses
When a decision rule must never be wrong, verification is worth paying for.
Paid support & enterprise verification
Support contracts and verification of critical logic where testing alone cannot close the risk.
Verified code generation
Integrate proof-carrying checks into code-generation pipelines so output arrives with a certificate.
Proof & model audits
Independent audit of proofs and models, plus sponsored development of the capabilities you depend on.
Get involved
Where the code stands
The licence is settled and the code is written. What has not happened is the push to a public remote. We would rather say that than link you to a 404.
Licence: EPL-2.0 or GPL-2.0-or-later with the Classpath exception. Clojure's own dual licence. It publishes with the release. In the meantime, the work you can read today is orhof, the operations-research library the prover is built to check, 251 functions, 30 namespaces, zero dependencies, MIT, and chachaml. If you want the prover sources before the release, ask and we will send them.
FAQ
Questions about Rainbow
What is Rainbow?
Rainbow is an open-source, Clojure-native theorem prover that treats terms, declarations, proofs, failures and provenance as inspectable, composable data. A small trusted kernel checks proof terms that an untrusted engine proposes, so a bug in the engine cannot produce a false certificate.
What does "proofs as data" mean?
A proof is an ordinary, immutable, content-addressed value. It can be stored, shared, versioned and audited like any other data, and terms and proofs compose: a verified result becomes a building block for the next one. An expensive parametric proof is produced once, and each subsequent decision carries a certificate the kernel re-checks cheaply.
What can Rainbow prove today, and what can it not?
It checks signed rational arithmetic, finite vectors and their operations, Bellman and value-iteration steps, and gradient methods, and it proves all 222 catalogued operations-research algorithms — the catalogue is complete, with nothing pending and nothing refuted. It does not yet claim infinite-horizon value-iteration convergence, Bellman fixed-point uniqueness, a proved correspondence to executing Clojure, or broad reconstruction of Mathlib. Where a result is not proved, the documentation marks it unproved.
How big is the trusted kernel, and why does that matter?
The trusted kernel is about 1,200 lines: the whole trusted base. The size of the trusted base is the size of what you must believe, and this one is small enough to read and audit. It is a trusted computing base: trusted on inspection, with its own metatheoretic soundness argued informally and never machine-checked.
What licence is Rainbow under, and can I read the code?
Open source, under the Eclipse Public License 2.0 or GPL 2.0-or-later with the Classpath exception: the same dual licence Clojure itself uses. The repository is not published yet; it goes public with the release. What you can read today is orhof, the operations-research library the prover checks, and chachaml. Ask us and we will send you the prover sources.
Who should care about Rainbow?
Teams with a decision rule that must never be wrong, where testing alone cannot close the risk. Commercial uses include paid support and enterprise verification of critical logic, proof-carrying checks inside code-generation pipelines, and independent audits of proofs and models.
Bring us a hard problem
If you have a rule that must never be wrong
Tell us where testing stops being enough. A partner will say whether formal methods and Rainbow can close the risk, and if they cannot, that is the reply.