Verification design

If you are looking for a practical guide, start with /docs/verification/design. This page covers three designs that are related but distinct: the exact engine's execution model and its Lean proof surface, and the trace-certificate machinery that checks protocols on both engines.

The exact execution model, mechanically

The exact engine's unit of state is the logical process (LP). Every event carries the key (time_ns, phase, origin_node, origin_sequence): time first, then a phase that orders event kinds at equal times, then the creator's identity and per-origin sequence number. Keys are totally ordered, and canonical serial execution (repeatedly execute the least pending key) defines the reference semantics.

Parallel execution proceeds in safe-horizon rounds: each round computes a horizon from certified channel delay bounds, every active LP drains its own pending events below that half-open horizon in key order, remote events are exchanged at a barrier, and the exchange merges them canonically. The implementation lives in executor/src/event.rs and executor/src/safe_horizon.rs.

Terminology is deliberate throughout these docs: actor / model / mailbox describe the legacy Nexosim engine; LP / image / event / transition describe the exact executor. The exact engine is not an actor runtime: its protocols are compiled state machines over an immutable image.

The proof surface

Trace replay is not the only mechanized story. The lean/DaysExecutor* development proves five theorems about the execution machinery itself: the validity of the shipped horizon policy, serializability of each round and of whole runs, the service-start discipline those equalities require (with executable countermodels showing each clause necessary), and the intra-round reordering license that lets device backends batch work. An audit driver checks that every declaration these theorems reach rests only on Lean's three standard axioms.

Trace certificates: workflow and trust boundary

LeanGuard follows an untrusted producer / trusted checker model: Days (either engine) is an untrusted trace producer; the checker (Lean executable + Lean kernel) is the trusted consumer. This shrinks the trusted computing base: you do not need to verify the simulator runtime, only that the emitted certificate matches the reference semantics.

Canonical order is part of the specification

Trace rows can be emitted in nondeterministic file order due to concurrency and buffering, so acceptance is defined over a canonicalized trace. The canonical key differs by lineage:

• Legacy protocol families sort rows by (time_ns, event_id) and reject duplicate keys. Canonicalization costs O(n log n) before the linear replay.
• Days AGO families (tcp_check, sp_check, p10c_*) key on the full EventKey (time_ns, phase, origin_node, origin_sequence); several strict-order checkers require the trace to arrive already in canonical order and reject otherwise, so the sort-based cost model does not apply to them.

See also: /docs/reference/traces/schema.

Trace certificate contract

A trace family is a self-contained replay certificate: each semantic transition point emits exactly one row containing enough information to deterministically replay that transition and, when applicable, compare the checker-computed post-state to a logged snapshot. A row carries:

• When/where: simulation time and stable component identity.
• What happened: an event kind selecting the transition rule.
• Guards and parameters: values needed to evaluate gates/thresholds; the checker rejects parameter drift.
• Witness/snapshot: a compact legality witness, or an explicit post-state snapshot for deterministic replay.

Acceptance is canonicalize-and-replay: parse (keeping line numbers for diagnostics), canonicalize per the family's lineage, fold a partial step function, and return ACCEPT or REJECT with the first failing row.

Reusable obligation patterns

Across protocol families the same obligation classes recur, and they are what make new checkers cheap to add:

• ParamFreeze: record per-component parameters on first use; reject later mismatches.
• MonotoneTime: per-component time monotonicity under canonical order.
• PendingMatch: pending maps for paired events (send/recv, enqueue/dequeue).
• Gate: interval/cooldown/refresh/epoch gating rules.
• Accounting: nonnegativity and conservation for counters.
• SnapshotEq: recompute post-state under explicit encodings and compare to the logged snapshot.