Your agents forget. Mnema remembers.

The real CRDT implementation is compared with an independent reference fold. The checker enumerates every delivery order through seven operations per scenario (7! = 5,040), then runs a deterministic 3,000-schedule sample for larger cases. It checks causal delivery, convergence, liveness, and idempotence at the implementation layer.

const EXHAUSTIVE_MAX: usize = 7;
const SAMPLE_ORDERS: usize = 3000;

for_each_schedule(ops.len(), |perm| {
    replica.ingest(one_op_at_a_time(perm));
    assert_eq!(replica.materialize(), canonical);
});

Kani harnesses cover selected pure invariants over their stated symbolic bounds, including merge laws, add-wins resolution, clock monotonicity, and the recall cost ladder. TLC checks a finite three-replica model for consistency, convergence, causal behavior, GC safety, trust, and liveness. Every bound is stated in the property catalog, so each result is reproducible exactly as claimed.

\\* Finite protocol model; invariants named in the spec.
INVARIANTS == {
  Consistency,
  Convergent,
  Causal,
  Unforgeable,
  GCSafe
}

A frame length is read from disk and must be treated as untrusted. The Zi component proves the remaining-bytes form equivalent to the naive bound while keeping the host calculation overflow-safe. The surrounding Rust still owns byte reads, CRC, JSON, chain checks, and truncation.

fn frame_fits (off: Int) (header: Int)
              (payload_len: Int) (buf_len: Int) -> Bool
  req off + header <= buf_len
  ens result == (payload_len <= buf_len - off - header)
  ens result == (off + header + payload_len <= buf_len)
{
  ret payload_len <= buf_len - off - header
}