Formal Verification and Trace Validation

CCF’s formal models are written in Lean and live under lean/. Apart from the shared common package, each package contains an executable model of part of CCF, safety properties stated as theorems about that model, machine-checked proofs of those properties, and a replayer that checks traces recorded from the C++ implementation against the model.

The models and the implementation are connected in two different ways, which provide different guarantees:

• Proofs establish properties of the model for every execution the model allows. Lean’s kernel checks proof terms but accepts proofs that depend on declared axioms. The package CI lake check command also checks axiom dependencies, rejecting unfinished proofs and any axioms other than Lean’s standard propext, Classical.choice and Quot.sound. Each safety theorem is accompanied by a witness lemma showing that its premises can be satisfied, so that no property holds vacuously.

• Trace validation replays executions recorded from the C++ implementation, step by step, through the model’s transition function. A successful replay shows that the model can explain that particular recorded execution. A rejected trace is reported with a diagnostic identifying the record that the model cannot explain, which may reveal an implementation bug, a model error, or an instrumentation error.

Important

A theorem about a model is not a theorem about the C++ implementation. Trace validation checks only the executions that were recorded, and relies on the instrumentation recording them completely and accurately. None of the models cover liveness.

Lean packages

Package	What it models	Trace validation
common	Protocol-independent infrastructure shared by the other packages: transition systems, multi-node message-passing composition, finite and infinite execution traces, a trace event parser, and import coverage and architecture checks.	Not applicable.
consensus	The CCF consensus protocol, as implemented in src/consensus/aft/cft.h. Proved properties include election safety (no two primaries in the same term), prefix-comparability of committed logs, and that every positive commit index points to a signature entry. A joining node may initialize from another node’s committed ledger prefix, as when installing a snapshot; the join protocol is not modelled.	consensus-replay replays traces of the consensus scenarios run by the native cft_driver.
consistency	CCF’s externally visible consistency semantics, including transaction status, for a simple append-and-read application with forwarded reads, elections and invalidation. The primary guarantee is that committed writes serialize in transaction ID order, and that this order respects the real-time order of requests and their initial responses. There is no refinement proof connecting this model to the consensus model.	consistency-replay replays client-observed request, response and transaction status traces from a multi-node e2e test.
disaster-recovery	The recovery decision protocol (src/node/recovery_decision_protocol.cpp). Proved properties include that all quorum openings in a trace originate from one node and, under stated premises, that the opening node passes the consensus vote freshness check against a strict majority of the recovered ledgers.	disaster-recovery-replay replays node logs from e2e recovery scenarios.
kv	The observable semantics of CCF’s single-node key-value store (src/kv/), including snapshots, globally committed views, atomic application, compaction and rollback. Proved properties include serializability of normal observations and preservation of the committed prefix across rollback. See KV Implementation Model for the full contract and its proof and trust boundaries.	kv-replay replays traces recorded by the instrumented C++ KV unit tests, including a seeded concurrent fuzzer.

The README of each package lists the precise theorem statements, the scope of the model, and what a successful replay does and does not show.

Trace sources

Each replayer consumes traces produced by existing C++ tests:

• Consensus: the cft_scenario_test test runs tests/cft_scenarios_runner.py, which executes each scenario in tests/cft_scenarios/ with the cft_driver binary (src/consensus/aft/test/driver.cpp). The driver exports consensus events as Fluentd records with the ccf.cft tag, which the runner collects and writes as NDJSON traces to consensus/raw/ in the build directory.

• KV: building with -DCCF_KV_TRACING=ON enables test-only trace capture in kv_test. tests/kv_trace_validation.py captures the purpose-built KV trace * test cases and a seeded concurrent fuzzer, then checks every trace with kv-replay unless --capture-only is passed. Tracing is disabled in normal builds.

• Consistency: the consistency_trace_validation e2e test (tests/consistency_trace_validation.py) starts a three-node network running the basic_tv JavaScript application, and runs tests/tvc.py against it to record client requests, responses and transaction statuses to consistency/trace.ndjson. The test suspends the primary to cause an election during the recording.

• Disaster recovery: nodes started with the CCF_RECOVERY_TRACE environment variable set log each step of the recovery decision protocol as an RDP_TRACE record. These scenarios only run in the SNP Genoa CI job, where tests/infra/recovery_trace.py replays the node logs of the quorum, failover and multiple-timeout scenarios in tests/e2e_operations.py through disaster-recovery-replay.

Every replayer is also checked against committed fixtures: valid traces that it must accept and invalid traces that it must reject.

Continuous integration

The Lean workflow runs on pull requests that change the Lean packages, the consensus or KV implementation, or the trace tests.

• A package job for each of common, consensus, consistency, disaster-recovery and kv runs the kernel and axiom check (lake check), import coverage and architecture checks, formatting and linting, and, where applicable, the package’s replay fixtures.

• Separate capture jobs build CCF and record consensus, KV and consistency traces from the tests described above.

• Replay jobs build each replayer and validate every captured trace.

• A final Lean models and proofs job succeeds only if all of the above succeed.

The disaster recovery traces are replayed by the SNP Genoa job in the main CI workflow instead, since that is where the recovery scenarios run.

A separate Lean Mathlib equivalence workflow proves that the replacements for Mathlib definitions in lean/common are equivalent to the Mathlib originals, and runs only when those definitions change; see lean/mathlib-equivalence/README.md.

Running locally

Install Lean with elan. The Lean toolchain is pinned by lean/lean-toolchain, and the models are independent of normal CCF builds. From a package directory under lean/, the common checks are:

lake build --wfail --fail-fast
lake check --inadvisably-no-sandbox
lake exe check-imports
lake lint

To check formatting of all tracked Lean files, run scripts/lean-format-checks.sh from the repository root, optionally passing a package name.

lake check --inadvisably-no-sandbox performs the kernel and axiom checks. The flag disables build isolation so the package can use the shared common modules; only run this command on code you trust. The consensus package recommends running it only in CI. Each package README lists its complete validation commands, including how to build its replayer, replay its fixtures, and generate and replay traces from a local CCF build. For the KV model, see also Reproducing a run.

The trace viewer steps through recovery decision protocol traces as the Lean model replays them.

Background

The approach of validating the implementation against formal specifications in CI is described in the 2025 paper Smart Casual Verification of the Confidential Consortium Framework (see Research). The specifications described in that paper were written in TLA+; they have since been removed from the repository and replaced by the Lean models described on this page.