Reference

The manual pages and the design of the engine.

---

• Design: the world encoding, where actions come from, durability, search, properties, gates and limits.
• cmc(1): the command line.
• libcmc(3): the C interface for in-process models, the engine’s calibration path: cores, events, effects, properties, running a check.
• cmc(7): the model and the rules that keep a pass meaningful.
• The model file: the declarative file that points libcmc at the binary you ship, the environment to explore, and the invariants to check (the reasoning is in the decision record).
• The abstract model: a declarative .cml specification libcmc checks on its own (cmc --spec), bridges to TLA+ (cmc --emit-tla), and checks the shipping binary against by refinement (cmc --refine).
• When libcmc fits: where an explicit-state checker of the shipping code is the right tool, and where it is the wrong one.

After make install these are on your system as man cmc, man libcmc and man 7 cmc. The header, include/cmc.h, is the whole public API.

---

Table of contents

• Design
• cmc(1)
• libcmc(3)
• cmc(7)
• The model file
• The abstract model (.cml)
• Plan: TLA+ scope over the shipped code