Background
The research libcmc grew out of, the review that hardened it, and its calibration.
---The survey that led to libcmc’s design, the adversarial review of its actor mode with the fix for each finding, and its calibration against TLC, all from 2026-11-02. The current design is Design.
- Survey and original design
- Adversarial review of actor mode
- Calibration against TLC
- Process mode M0 – a prototype toward checking code written as it ships
- Process mode M1 – canonical state and a real search over interleavings
- Process mode M2 – a real malloc heap, and the boundary it draws
- Process mode M3 – a model file drives the checker
- Process mode M4 – multi-node, the checker owns the network
- Process mode M5 – time is an environment action (leader election)
- Process mode M5b – absolute time is engine-controlled (stale lease)
- Decision: one engine, a model file, the shipping binary
Table of contents
- Survey and original design
- Adversarial review of actor mode
- Calibration against TLC
- Process mode M0: catching a bug in code written as it ships
- Process mode M1: canonical state and a real search
- Process mode M2: a real malloc heap, and the wall it hits
- Decision: one engine, a model file, the shipping binary
- Process mode M3: a model file drives the checker
- Process mode M4: multi-node, the checker owns the network
- Process mode M5: time is an environment action
- Process mode M5b: absolute time is engine-controlled