Caelum¶

Caelum is an LTL model checker. You describe a system as a finite state machine — some variables and the rules for how they change — and you write down the properties it must always obey. Caelum then explores every state the system can reach and checks each property against all of them. When a property can be broken, Caelum hands you a counterexample: a concrete step-by-step trace showing exactly how it goes wrong.

Think of it as exhaustive testing for the logic of a system. Instead of the handful of scenarios you would think to write as unit tests, Caelum tries them all.

let x ∈ 0..3

init { x = 0 }

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

property in_range     { □ (x ≥ 0 ∧ x ≤ 3) }
property returns_zero { □ ◇ (x = 0) }

That block above is a live editor. Press Check ▶ (or Ctrl-Enter) to run the checker right here in your browser — no install required.

What Caelum is¶

A checker for finite-state systems: variables over bounded ranges, enums, and booleans, evolving through transitions.
A checker of temporal properties written in Linear Temporal Logic (LTL) — statements about how a system behaves over time, not just in one state.
Exhaustive for safety: it proves “never” properties for every reachable state and every possible ordering of events, so the bug that only shows up under one unlucky interleaving has nowhere to hide. “Eventually” properties are searched for violations up to a bound; the explicit engine proves them too, on small models.
A tool that explains failures: every failed property comes with a counterexample trace you can read.

What Caelum is not¶

Not a general theorem prover. It reasons about a specific finite model, not arbitrary mathematics.
Not for unbounded or large data. The state space must be finite and small enough to explore. It is a poor fit for heavy arithmetic, floating point, or big data structures.
Not sampling-based testing. It does not run your real program on example inputs; it checks a model of it, symbolically.
Not a programming language. A .lum file describes behaviour and requirements; it does not compute results.

Features¶

LTL model checking with always, eventually, next, and until operators
Counterexample generation showing exactly how a property fails
Three syntax modes: keyword (always), ASCII ([]), and Unicode (□)
Runs in your browser via WebAssembly — every example in these docs is a live, editable, verifiable editor
Modular specifications with imports
JSON output for integration with other tools
Deterministic formatter for consistent code style

Where to start¶

Never model-checked anything before? Read What Caelum Is For to learn what kind of problem this is good for.
Ready to try it? Trying Caelum in Your Browser explains the in-browser editor, then the Tutorial: A Traffic-Light Controller builds a real specification from scratch.
You can do the entire tutorial in your browser — installing the command-line tool (Command-Line Usage) is only needed to run specs offline or in CI.

Real World Examples

NFS Shared Lock