Command-Line Usage

Everything in the Tutorial: A Traffic-Light Controller runs in your browser, but installing the caelum binary lets you check specifications offline, script them, and wire them into CI.

Installation

Prerequisite: the Rust toolchain (edition 2021 or later).

git clone https://github.com/dhilst/caelum.git
cd caelum
cargo build --release

The binary is at target/release/caelum.

Your first check

Create a file called counter.lum:

module examples.counter

const max = 3

let x ∈ 0..max

init {
  x = 0
}

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

property in_range {
  □ (x >= 0 ∧ x <= max)
}

property returns_to_zero {
  □ ◇ (x = 0)
}

Run it:

caelum counter.lum

Both properties pass. The counter wraps around from max back to 0, so it always returns to zero and always stays in range.

Reading the output

On success, Caelum prints a summary line and one line per property, and exits with code 0:

OK loaded 1 file(s), typechecked 5 item(s), built 4 reachable state(s) and 4 transition edge(s)
PASS property in_range
PASS property returns_to_zero

On failure, the summary line starts with FAIL, each broken property is listed, and the process exits with code 1. Add --show-trace to print the counterexample for each failing property:

FAIL property never_two
counterexample:
  s0: x = 0
       --(step)-->
  s1: x = 1
       --(step)-->
  s2: x = 2

Each --(name)--> arrow names the transition that fired between two states. For a liveness property the trace ends in a loop, marked cycle starts at sN.

Usage

caelum [OPTIONS] [SPEC]
caelum <COMMAND> [OPTIONS] <SPEC>

When no subcommand is given, caelum <spec>.lum is equivalent to caelum check <spec>.lum.

Commands

check

Parse, validate, build the transition system, and check all properties.

caelum check spec.lum
caelum check --format json spec.lum
caelum check --show-trace spec.lum

parse

Parse the specification and report any syntax errors. Does not build the model or check properties.

caelum parse spec.lum
caelum parse --format json spec.lum

fmt

Parse and print the specification in normalized form.

caelum fmt spec.lum
caelum fmt --print-keywords spec.lum
caelum fmt --print-ascii-operators spec.lum
caelum fmt --print-unicode-operators spec.lum

Formatting is idempotent: formatting an already-formatted file produces identical output.

Options

Flag	Description
--format human|json	Output format (default: human)
--engine explicit|bmc	Checking engine (default: explicit). bmc runs bounded model checking.
--solver varisat|cadical|z3	SAT backend for the bmc engine (default: z3). Requires the matching Cargo feature to be compiled in; z3 links the system libz3 (install libz3-dev / the z3 package).
--bmc-depth N	Unrolling depth for the bmc engine (default: 50)
--prove (alias --k-induction)	Attempt k-induction to certify safety properties under --engine bmc
--show-trace	Display counterexample traces on failure
--dump-graph	Print the reachable transition graph
--max-states N	Limit state exploration (default: 100,000)
--include-path DIR	Additional import search directories
--print-keywords	Format with keyword operators (always, and)
--print-ascii-operators	Format with ASCII operators ([], /\)
--print-unicode-operators	Format with Unicode operators (□, ∧) (default)

Exit Codes

Code	Meaning
0	The specification parsed and all checks passed
1	One or more properties failed
2	Parse error
3	Semantic validation error
4	Import or file loading error
5	Model construction error
6	Internal error

If multiple error classes occur, the earliest pipeline stage determines the exit code.