History and provenance

The research libcmc grew out of, the review that hardened it, its calibration, and the process-mode lab notebook.

---

This is a lab notebook, not a roadmap: the survey that led to libcmc’s design, the adversarial review of its actor mode with the fix for each finding, the calibration against TLC, and the process-mode milestones as they were built. Every milestone below is done and shipped; the pages are dated records of work already in the engine. For the tool as it is, start at Design, the model file and the examples.

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)
Process mode M6 – crash loses volatile, keeps durable (lost commit)
Process mode M7 – honest verdicts, and what Paxos costs
Decision: one engine, a model file, the shipping binary

History and provenance

Table of contents