cmc(1)

explicit-state model checker for C protocol code

---
CMC(1) General Commands Manual CMC(1)

cmc — explicit-state model checker for C protocol code

cmc --model-file file [--binary path] [--bfs | --simulate] [--seed n] [--walks k] [--depth d] [--max-states n] [--time seconds] [--crashes n] [--drops n] [--timeouts n]

cmc --spec file [--define tag ...]

cmc --emit-tla file [--define tag ...]

cmc --refine spec --bind file [--refine-steps] --binary path [--model-file file] [--simulate]

cmc --model name [--tlc-cfg file | --cfg key=value[,...]] [--inv name[,...]] [--prop name[,...]] [--all-props] [--bfs | --dfs depth | --simulate] [--seed n] [--walks k] [--depth d] [--det] [--max-states n] [--time seconds] [--trace-out file] [--progress seconds] [--quiet] [--coverage] [--clients n] [--drops n] [--dups n] [--crashes n] [--net-cap n] [--persist-cap n] [--reply-cap n] [--net fifo | bag] [--live-steps k]

cmc --replay file [--inv names | --all-props]

cmc --model name --list

cmc --version

cmc explores every interleaving of a set of protocol nodes, the network between them, their timeouts and their crashes, up to the budgets given, and checks the properties in every state it reaches.

With --model-file, the nodes are the program you ship, run unmodified as processes; the model file names the program, the environment to explore and the invariants. That is the way to check a product; see Checking a program below, the model file, and cmc(7).

With --model, the nodes are an in-process model: C step functions written against libcmc(3). That interface is the engine's calibration path: the hc core reproduces TLC's results on a published consensus specification. The rest of this page, from Choosing the model and properties, describes it.

make install installs cmc. A program that embeds the engine with in-process models of its own writes a () that passes its table of models to (), and links against libcmc.a; that program is a cmc too. The binary built by this repository carries the in-process models hc (the calibration core), toy, and toy-bug1 to toy-bug3.

Output follows the wording of TLC, the TLA+ model checker, so the two can be compared line by line. Depth counts the initial state as 1.

file
Check the program the model file names, with its environment and invariants. Linux x86-64 only: the nodes run under seccomp user notification. Every key the file sets must be one cmc implements; an unknown or unsupported key is an error, not ignored.
path
Check this program instead of the file's binary, for example a build with a planted bug. It must be a non-PIE executable (built with -no-pie).
file
Model-check an abstract specification (a .cml module) on its own, the way TLC checks a TLA+ module: no implementation, just the declared variables, actions and invariants. See the TLA+-scope plan.
file
Translate the abstract specification (a .cml module) to TLA+ on standard output, so it can be checked with TLC or Apalache and proved with TLAPS. Name the output after the module (NAME.tla) so TLC accepts it.
tag
Activate an action gated with [tag] in a .cml spec; repeatable. Used to turn on a planted-bug action.
spec
Check that the implementation named by --binary or the model file the abstract spec (a .cml module). At each reached implementation state the abstract invariants are checked against the mapped state, so one abstract model validates many implementations. Requires --bind.
file
The binding (a .bind file) that maps the implementation's observables onto the abstract variables, for --refine.
Check refinement at the level of , not only states (Milestone C2): each implementation transition must map to an abstract action step or a stutter (the abstraction unchanged). This catches a step the abstract model forbids even when every state it reaches satisfies the invariant, which --refine alone cannot. Requires --refine, and every spec variable must have a ([map]) entry (it refuses otherwise), since matching an abstract action step needs the whole abstract state.
n, --drops n, --timeouts n
Override the file's budgets.
d
Bound the search to d actions; a search that reaches it is reported as incomplete. With --simulate, the length of each walk, default 100.

--bfs, --simulate, --seed, --walks, --max-states and --time work as for in-process models, except that walk i of a simulation does not take its own seed: the same --seed takes the same walks. Any other option with --model-file is an error.

name
The model to check, by its name in the program's model table. Required, except with --replay.
key=value[,...]
Core settings, passed to the core's (). May be given more than once; later settings override earlier ones, including those read by --tlc-cfg.
file
Read a TLC .cfg file: its become core settings, and its and become the properties to check.
name[,..., --prop name[,...]]
Check these properties. The two options are synonyms; each property's kind comes from the model.
Check every property of the model.
Print the model's property names and exit.
Print the libcmc version and exit.

A model may mark its first properties as always checked. At least one property must be named, or --all-props given.

Breadth-first search, the default. It finds a shortest counterexample, and its state counts are exact.
depth
Depth-first search to depth states. A search that reaches the bound without finishing is reported as incomplete, never as a pass.
Seeded random walks, not exhaustive. Walk i uses seed n+i; a violation is reported with the --seed and --walks 1 that reproduce it.
n
First seed for --simulate. Default 0.
k
Number of walks for --simulate. Default 1000.
d
Length of each walk, in states. Default 100.
file
Run a replay file written by --trace-out through the real cores, printing each state. The model, settings and budgets are taken from the file; an option on the command line that conflicts with the file is refused.
Determinism gate: run every step twice from copies of the same state and fail if the two runs differ in their outputs or their next state.
n
Stop after n distinct states.
seconds
Stop after seconds of wall time.

These options apply to message-passing cores (actor mode). Each budget is a count over the whole run, from 0 to 255.

n
Client requests each node may receive. Default 1.
n
Messages the network may lose. With --net fifo, a drop resets the connection and both ends are told. Default 0.
n
Messages the network may duplicate. Needs --net bag. Default 0.
n
Crashes, of any node. A crash keeps any prefix of the node's pending disk writes, loses the rest and the volatile state, resets its connections and restarts it. Default 0.
n
Messages in flight at once. Default 8.
n
Pending disk writes per node. Default 2.
n
Client replies recorded in the ghost log. Default 8.
fifo |
, the default, has one ordered channel per pair of nodes, as TCP does, and never duplicates. bag is an unordered multiset that may duplicate.
k
Bound, in steps of the fair schedule, for eventually-properties. Default 1000.

Going past a cap is reported as an engine error, never silently truncated.

file
On a violation, write the counterexample as a replay file.
seconds
Print a progress line every seconds during breadth-first search; 0 turns it off. Default 60.
Do not print the counterexample.
Print, for each action kind, the states it generated and the new distinct states it found.

The path of cmc-preload.so, the library every checked node runs under. By default it is found beside the running program (a build tree), then in ../lib/libcmc from it (an installed bin/cmc). A program of your own that calls cmc_main() must set it. A node it did not load into is an error.

*.model
Model files; see the model file.
cmc-preload.so
A deterministic heap and a logical clock for the checked program.
*.replay
Replay files. A header names the model, settings and budgets; each following ‘act’ line is one action in hexadecimal, with its description as a comment.

0
No property was violated, and the search was complete for its mode: breadth-first or depth-first search finished, the walks ran, or the replay ended.
1
A property was violated, an engine rule was broken (determinism, durability, a cap), or a witness was never reached.
2
Incomplete: a state, time or depth limit stopped the search before it finished, with no violation found.
3
Usage error, a bad setting, a model file that cannot be used, or a replay file that cannot be run.

Check a server as it ships, then a build of it with a planted bug:

$ cmc --model-file kvserver.model
...
Model checking completed. No error has been found.
$ cmc --model-file kvserver.model --binary ./kvserver-bug
Error: Invariant no_lost_ack is violated.
...

Check every property of the toy lock server, an in-process model:

$ build/cmc --model toy --all-props
...
Model checking completed. No error has been found.
...
49 states generated, 34 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 11.

Find the planted bug in toy-bug1, save the counterexample, and replay it:

$ build/cmc --model toy-bug1 --inv Mutex --trace-out bug1.replay
Error: Invariant Mutex is violated.
  2 clients in the critical section
...
$ build/cmc --replay bug1.replay --inv Mutex

Check a calibration configuration against its TLC result:

$ build/cmc --model hc \
    --tlc-cfg calib/hc/cfg/hc_paper_cp_n3_s1.cfg --det

Search a large space by random walks first:

$ ./mycmc --model mymodel --all-props --crashes 1 --drops 1 \
    --simulate --seed 7 --walks 100000 --depth 60

libcmc(3), cmc(7)

The guide and design notes: https://gregburd.codeberg.page/libcmc/

Greg Burd <greg@burd.me>

A pass covers only the budgets given. Raise --clients, --drops and --crashes until the bugs you planted are caught, and treat a run stopped by --max-states or --time as "no violation found in N states".

--net bag allows behaviour a FIFO transport never shows, so a counterexample found in bag mode may be spurious for a protocol that relies on FIFO order.

November 5, 2026 Debian

mdoc source: man/man1/cmc.1