Maturity levels

Every Rainbow result has a level from 1 to 6. A chain of results gets the level of its weakest link.

Level 1: research record

The work exists and is written down. Nobody claims that anyone else can run it.

Level 2: reproducible artifact

Anyone can run it again from the repository and get the same result. lein verify replays a checkpoint, and the kernel checks each declaration as it loads. lein reproduce rebuilds a milestone’s checkpoint from source and compares content ids.

Level 3: proved theorem about a model

A theorem about a mathematical model, checked by the kernel with no axioms: natural numbers, rationals, finite sums, an algorithm’s specification. It says nothing about a program that runs. Most of the open core is Level 3.

Level 4: checked output

A real program produces an output, and the kernel checks that output against a proved statement. If the program has a bug, you get a refusal, not a wrong answer. Only the outputs that were checked are covered, not the program.

Level 5: program proved to meet its specification

The program exists as data, and a kernel-checked theorem says it does what the specification says. A printer turns it into code that runs. Every theorem about the specification that holds for all inputs also holds for the program. Some link between the proof and the running code is reviewed by people rather than proved.

Level 6: checked by machine down to the running code

Every link from the specification to the code that runs is checked by machine, except a published list of items small enough to audit by reading: the trusted base. A program that reads sensors, messages or clocks also states its assumptions about the world as premises. Each step is checked while the program runs, and if a check fails, the program falls back to a safe action.

What sets the level

Tests never count, at any coverage. A test compares an output with a value a person chose, and a change that breaks both the same way still passes.

One unproved step that is not on the trusted-base list sets the level of the whole chain. There are no half levels.

Levels 4 to 6 in Rainbow Pro

Rainbow Pro writes the program from your specification together with its proof, and the open kernel checks that proof. Of the 1,000 program families in Pro, 995 are at Level 5: the code is proved to do what its specification says, for every input.