# Current scope correction — 20 September 2026

The historical inventory below combines formal declarations, model checks and runtime tests.
It must not be described as a count of independent proofs of production correctness.
Z3 includes both satisfiable consistency checks and unsatisfiable counterexample searches;
Z3 and Dafny encode separate models rather than importing the deployed Python engine.
TLA+ concerns a proposed architecture, not a specification linked to the live deployment.

The toolchain availability statement in the September 3 history below was superseded by the
successful September 10 build records published as `REVERIFY_20260910.log` and
`REVERIFY_20260910_hypothesis.log`. Those are dated runs, not a claim that every property
holds or that every artifact was compiled again today. The September 20 HTTPS readback
verified every manifest artifact hash. A binary header alone does not prove source correspondence.
The original pinned artifacts and manifest have not changed.

---

## Historical restoration record and subsequent corrections

# KAIROS DAG V5 — FORMAL VERIFICATION CORPUS

**Load-bearing artifacts — retained deliberately; do not remove.**

Origin: commit `f1d646f`, 2026-06-06 22:16:35 -0500 —
"FORTRESS: 225 verified proofs across 5 kernels (Lean/Coq/Isabelle/Dafny/Z3)",
corrected by `727ee61` — "all 7 provers, 225 formal + 30 system = 255 total".
That 255 is NOT reproducible by counting; see the correction below.

## What is here

| System | File | Lines | Named obligations |
|---|---|---|---|
| Coq | `KairosDAGV5.v` | 577 | 39 theorems/lemmas |
| Isabelle/HOL | `KairosDAGV5.thy` | 435 | 32 |
| Lean | `KairosDAGV5.lean` | 226 | 38 |
| Dafny | `KairosDAGV5.dfy` | 344 | 27 |
| TLA+ | `KairosDistributed.tla` | 221 | 10 stated; model-checked 2026-09-06: 5 hold, 5 refuted (`tla_recheck_20260906/REPORT.md`) |
| Z3 | `z3_verify_dag.py` | 547 | — |
| system/runtime/fuzz | `system_verify_all.py`, `runtime_verify_dag.py`, `hypothesis_fuzz_dag.py` | 1,409 | — |

`KairosDAGV5.vo` (55,053 bytes, magic header `Coq!`) is Coq's COMPILED proof
object. It cannot exist unless `coqc` succeeded on `KairosDAGV5.v`. `.glob`
(39,837 bytes of cross-references) and `.lia.cache` are further artifacts of a
real compilation. `ROOT` builds the Isabelle session against `HOL-Analysis`
with `quick_and_dirty = false`, which forbids `sorry` — no stubbed proofs.

## Why this file exists

These files were swept out of the working tree on 2026-08-25 by commit
`de3b047` ("crypto rail, moltbook bots, Stripe billing portal, ..."), a large
unrelated commit that removed all of `kairos-signal-main/`. They survived only
in git history.

Because nothing was on disk, two earlier audits recorded the corpus as
unsubstantiated. Both read the filesystem only; the artifacts were in git the
whole time. Verifying an artifact requires checking where it is actually
stored, which is why the restore below is stated against git blob hashes.

Restored 2026-09-03, all 16 files verified byte-identical to the `f1d646f`
blobs (sha256, 16/16). Integrity list: `MANIFEST.sha256`.

## Honest scope — read before publishing any number

* The correct claim is **237 obligations across 7 provers**, of which Lean is
  ONE (38). CORRECTED 2026-09-04: the "~255" figure traced to hard-coded
  per-prover print statements in `system_verify_all.py` which disagree with the
  files themselves (banner: Coq 32 / Lean 45 / Isabelle 30 / TLA+ 10; counted:
  39 / 38 / 32 / 8). The published table at /proofs is counted from these
  artifacts, and reads 237. The superseded site line, which named the wrong
  prover, is disowned rather than deleted. Do not repeat it in that form.
* Coq, Isabelle and Dafny are **not installed on this box**. The `.vo` proves
  the Coq side compiled in June 2026; nothing here has been re-verified since.
  Until the toolchains are installed and re-run, the publishable claim is
  "compiled under Coq/Isabelle/Dafny/Lean/Z3 as of 2026-06-06, artifacts
  retained" — NOT "reproducible on demand".
* The separate, currently-reproducible suite is
  `~/hyperliquid_paper/formal_verification/run_all.sh` (6 Lean files, 25
  theorems, Z3 duals). Keep the two corpora distinct; merging their counts
  would be an overstatement.

> Correction 2026-09-06: the TLA+ row is 10 properties (6 safety invariants + 4 liveness), not 8; counted total 237, not 235. Text above amended; proof artifacts unchanged and still byte-identical to MANIFEST.sha256.

> Correction 2026-09-06 (second): the 10 TLA+ properties were model-checked for the first time (TLC 2.19, labelled model, corpus file unmodified, sha256 ffdc3ca8…): 5 hold, 5 refuted — QueueBounds (unbounded `channel_ack`) and all four liveness properties (`WF_vars(Next)` only). Counted total stays 237 (stated); verified on this box 2026-09-06: 232. The runtime harness IS re-runnable: engine located, 38/38.