Verification & Research

This section is the research-oriented documentation. If you want to use the verification tooling, start with /docs/verification.

Three distinct verification surfaces coexist in this repository, and it helps to know which one a page is about:

1. Execution-model proofs (lean/DaysExecutor*): five Lean theorems about the Days AGO machinery: the safe-horizon bound family, round and run serializability, the service-start discipline, and the intra-round reordering license. These govern the executor itself.
2. Days AGO certificates: trace-level conformance for the Days AGO protocols (tcp_check, sp_check, and the p10c_* checkers), keyed by the full EventKey order.
3. Legacy LeanGuard CSV replay: the original certificate machinery for the legacy engine's floating-point protocols, keyed by (time_ns, event_id).

A note on evaluation claims in this section: pages distinguish shipped code (buildable from this tree), committed fixtures (runnable benchmarks such as the E5 and E6 families and the 262,144-flow frontier), and external campaign evidence (measured results recorded in the project's evidence archive, machine-qualified where cited). Results from fixtures not present in this tree are labeled as external.