A theorem prover built to check the methods we sell
Rainbow is written in Clojure. It keeps each proof as data that you can store and check again. A search engine proposes proofs and a small kernel checks each one, so a bug in the search engine cannot give a false proof.
What it can do today
Checked natively
- Signed rational arithmetic.
- Finite vectors and their operations.
- Bellman / value-iteration steps.
- Gradient methods.
The catalogue comes from our book Applied Higher Order Functions.
What is open and what is Pro
The kernel and the maths are open source. Rainbow Pro generates certified, correct code from a specification, for systems where an error costs a lot of money, harms people's health, breaks the law or exposes private data. Of its 1,000 program families, 995 come with a kernel-checked theorem that the code does what its specification says.
Open
- The trusted kernel and the list of what it rests on.
- The elaborator, the basic tactics, the proof search and its rewriting engine.
- The LP certificate checker, and two pages for auditors: the Proof Explorer and the LP Certificate Viewer.
- The proof corpus: rationals, finite sums, order, convexity, duality and the algorithm catalogue.
- The Lean bridge and the replayable checkpoints.
- The command line:
verifyre-checks a module’s theorems,reproducerebuilds a checkpoint from source. - Documentation: getting started, the proof language, guides and every proof.
Rainbow Pro
- Code generated from your specification, with a proof that it meets it.
- Certificates for the decisions your systems make, checked again on your side.
- Help from the people who build Rainbow. About Rainbow Pro
Pro runs on the open core as a library, so the open kernel checks each theorem that Pro proves.
What a check looks like
The slow, expensive proof is done once. After that, each decision comes with a certificate that the kernel checks again quickly.
;; 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 small trusted kernel is the only thing that decides.
(kernel/check gradient-step-decreases-loss proof)
;; => {:ok true :certificate #rainbow/cert "…content-addressed hash…"}How we can work with you on Rainbow
Paid support & enterprise verification
We support your team, or we verify the rules in your code that must not be wrong.
Verified code generation
Your pipeline generates code that comes with a certificate.
Proof & model audits
We audit your proofs and models. You can also pay us to build a feature you need.
Run it yourself
Clone the open core and re-check any theorem on your machine.
$ git clone https://github.com/flexiana/rainbow && cd rainbow
$ lein verify rainbow.math.finite.rational-argmax
checkpoint artifacts/ahof/d63-eligibility-traces/checkpoint.edn.gz replayed: environment sha256:a41ba35a9f845aa04600620234dd1ccbb86969b09ffb14a44847da82ba4a5d5c names sha256:04959786090003bdfd133d7f4da521566de7ede77813ee1fa8aa3185284d193a
OK rainbow.math.finite.rational-argmax (15 theorems: 13 for all inputs, 0 definitional unfoldings, 2 worked instances)
checked instance bool/false-not-true axiom-free
checked for-all decision/finite-nnrat-argmax-dominates axiom-free
...Real output from Rainbow.
orhof, the operations-research library the prover checks, is open source too.
Bring us a rule that must never be wrong
Jiri or Ivo will tell you what Rainbow can prove about it.