# KAIROS DAG V5 — FORMAL VERIFICATION CORPUS

**Do not delete. Do not "clean up". This is Dan's work and it is load-bearing.**

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 | — |
| 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, `SITE_CLAIM_AUDIT_20260806.json` and
`VERIFICATION_STATUS.md` both concluded the estate's proof claim was fiction —
"CONTRADICTED, nothing behind it exists". **That conclusion was wrong.** The
audit checked the filesystem and never checked git. An audit that looks at the
wrong evidence produces a confident false negative, and this one talked the
estate out of the strongest thing it owns for four months.

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 **235 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 235. 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.