Trying Caelum in Your Browser

You do not have to install anything to use Caelum. The whole model checker is compiled to WebAssembly and runs inside this documentation. Every .lum example you see is a live editor, and the entire Tutorial: A Traffic-Light Controller can be completed without leaving your browser.

Every example is editable and runnable

Wherever these docs show a .lum specification, that grey block is a real code editor, not a static snippet. You can:

  • Edit it in place — change a value, break a rule, add a property.

  • Run it — press the Check ▶ button or Ctrl-Enter (Cmd-Enter on a Mac).

A block gets a Check ▶ button when it contains at least one property (or invalid) to verify. Smaller fragments that only show a type or a transition are still editable and syntax-highlighted, but there is nothing to check, so they have no button.

Try it now — press Check ▶:

let x ∈ 0..2

init { x = 0 }

transition step { x' = (x + 1) mod 3 }

property stays_small { □ (x ≤ 2) }

Everything runs locally

The checker is caelum-kernel compiled to WebAssembly, using the pure-Rust varisat backend. Your specification is checked entirely in your browser — it never leaves the page, there is no server, and no account is required. Close the tab and it is gone.

Reading the results

When you run a spec, a results pane appears beneath the editor.

Passing. Each property is listed with a pass marker. A pass means Caelum explored every reachable state and found no way to violate the property.

Failing — the counterexample trace. When a property can be broken, Caelum shows a counterexample: a table with one row per state, the variable values in each, and the transition taken between rows. It is a concrete, replayable story of how the property fails. For a liveness (□ ◇) property the trace ends in a loop, and a ⟲ marker shows the state the loop returns to — the system cycles there forever without the good thing ever happening.

Try this one. The property claims x is never 2, but the counter reaches 2 on the third step, so it fails — press Check ▶ and read the trace:

let x ∈ 0..2

init { x = 0 }

transition step { x' = (x + 1) mod 3 }

property never_two { □ (x ≠ 2) }

Errors — inline underlines. If a spec does not parse or has a type error, Caelum underlines the exact spot and explains the problem, the same way an editor flags a syntax error. Try deleting the closing brace } from the property above and running it again.

The invalid keyword

Sometimes you want to confirm that a property does not hold — for example, to show a bad state is unreachable. Marking a block invalid flips the reporting: Caelum reports a pass when the property fails as expected, and a fail if it unexpectedly holds.

let x ∈ 0..2

init { x = 0 }

transition step { x' = (x + 1) mod 3 }

invalid never_reaches_two { □ (x ≠ 2) }

Here x does reach 2, so the property is genuinely false — which is exactly what invalid asserts, so this reports a pass.

Where to go next

  • The Tutorial: A Traffic-Light Controller builds a complete traffic-light controller step by step, right in these editors.

  • The Playground is a full-page blank editor for your own experiments, with the ability to load and share specifications by URL.