Every data vendor says their pipeline is sound. We wrote the invariants down as theorems and put them through Coq, Isabelle/HOL, Lean 4, Dafny, Z3, TLA+ and property-based fuzzing. The artifacts are on this page — source and compiled — so the claim does not rest on us saying it.
These numbers were produced by counting declarations in the files below on 2026-09-04, not quoted from a summary. The method is in the last column so you can repeat it.
| Prover | Obligations | Artifact | Counted as |
|---|---|---|---|
| Coq / Rocq 9.1.1 | 39 | KairosDAGV5.v · .vo (compiled) | Theorem|Lemma|Corollary|Proposition |
| Lean 4.32.2 | 38 | KairosDAGV5.lean | theorem|lemma |
| Isabelle/HOL 2025 | 32 | KairosDAGV5.thy · ROOT | theorem|lemma|corollary |
| Dafny 4.11.0 | 27 | KairosDAGV5.dfy | lemma|method|function|predicate |
| Z3 SMT 4.15.4 | 42 | z3_verify_dag.py | check_prop() calls, each unsat-of-negation |
| Runtime (DAG) | 38 | executed against production source | check functions |
| TLA+ | 8 | KairosDistributed.tla | invariants + temporal properties |
| Hypothesis (PBT) | 11 | hypothesis_fuzz_dag.py | @given properties |
| Total | 235 | MANIFEST.sha256 | 136 theorem-proved in 4 provers |
The compiled Coq object KairosDAGV5.vo is 55,053 bytes and begins with the magic
bytes Coq!. That file cannot exist unless coqc accepted the source. The
Isabelle session runs under quick_and_dirty = false, which means no sorry
was permitted anywhere in it — check ROOT yourself.
curl -O https://kairossignal.com/proofs/MANIFEST.sha256
curl -O https://kairossignal.com/proofs/KairosDAGV5.v
curl -O https://kairossignal.com/proofs/KairosDAGV5.vo
sha256sum -c MANIFEST.sha256 # our hashes, your machine
coqc KairosDAGV5.v # if you have Coq 9, reproduce the .voTwo facts, stated side by side rather than one hidden behind the other.
| Layer | Last verified | Reproducible on demand |
|---|---|---|
| Lean 4 — 25 theorems over the five production invariants, plus 28 Z3 / property cases | 2026-09-04, exit 0 | Yes — runs in CI on every change |
| Coq · Isabelle · Dafny corpus (98 obligations) | 2026-06-06, artifacts retained | Not on our box — those three toolchains are not installed here |
So the precise sentence is: the Lean and Z3 layers re-run green today; the Coq, Isabelle and Dafny corpus compiled in June and its artifacts are published above. We will not write "reproducible on demand" over the second row until the toolchains are back and it runs green. If you have Coq 9, Isabelle 2025 or Dafny 4.11 installed, you can reproduce it before we can — and we would rather you did.
They are about our machinery, not about markets. They do not predict anything, and we do not sell them as edge. What they buy is narrower and more useful: when we say a value was not constructed with look-ahead, that a gate failed closed, that a derivation graph is acyclic, or that a cost identity holds — those are kernel-checked properties, not assurances from a vendor.
The same discipline runs against the live product daily. Our claim checker grades every published number on this site against live truth and fails in both directions, because overstatement and understatement are both errors. When our dilution engine served a septillion-dollar FDV, the fix shipped with the correction attached to the value, naming the source we rejected.
Two corrections we are keeping visible. This site previously said "250 Lean proofs" — right order of magnitude, wrong prover, and stated with confidence it had not earned. Then an internal audit went wrong the other way: it checked the filesystem, found the proof directory missing, and called the corpus fiction — without checking git, where an unrelated commit had swept it out of the working tree. The files were recovered 2026-09-03, sixteen of sixteen byte-identical to the git blobs. And the summary banner in our own verifier hard-coded per-prover counts that disagree with the files; the table above is counted, which is why it reads 235 and not the 255 we previously published.
Institutional tier → Verify our live data → Corpus provenance →
Obligation counts produced by direct declaration counts over the published artifacts
on 2026-09-04. Live layer re-run 2026-09-04T00:41:25Z, exit 0. Corpus provenance: propintel commits
f1d646f / 727ee61, 2026-06-06.