[FINDING] Doc-drift rollup: stale counts and refs across the FV evidence docs (Kontrol 33, Halmos 42, KAT 12, HW 14, TLA 17, checkct 5, Certora zombies, KAT sync)

[Nicola-Ceornea]

Surface: docs · Severity: low (all understatements/conservative direction, but they post-date re-measures and prove the ledger gate blind to this class) · Evidence: executed greps/counts · Target: f91aa82

• AXIOM_STATUS.json:327 A3.2 artifact says "4/4 rules PASS" (2026-06-15) while the same entry's status_detail says 7/7; THE_CLAIM.md:76,130 "30 KEVM proofs" vs 33 (run_kontrol.sh EXPECTED_PROOFS=33; grep -c 'function prove_' = 3+8+6+9+7). The ledger checker pins artifact count only — structurally blind to evidence-prose drift.
• PINNED_CODEHASHES.md:21 + DEPLOYED_BYTECODE_PIN_CAVEAT.md:131 "38/38" vs 42-rule floor (run_halmos.sh EXPECTED_RULES=42); PinnedCodehashes.t.sol:42-48 "19 rules PASS"; "each 10/10" vs the 12-vector corpus.
• AXIOM_STATUS.json A3.2 carries two zombie certora-rule-set discharge artifacts — no date, no evidence, certora not installed, no Make target, no gate enrollment (the exact failure mode PINNED_CODEHASHES.md:88 documents for A3.4).
• KONTROL_SCOPING.md:87 still says "Halmos stays as the fast CI gate" — contradicts its own line 25 and the recorded HALMOS-FAST-CI-GATE-FALSE correction.
• HW_ASSUMPTIONS.json has 14 rows (map row 14 says 12; 3/14 have runnable falsifying tests).
• tla/README.md:27-28 "16 expected outcomes" → 17; :60 "5 pinned configs" → 6.
• docs/STATUS.md:351,415 + Makefile:4363 + docs/tooling-and-systems.md:52 say 4 SECURE checkct drivers — actual 5 (+1 by-design insecure control) since 59ec0af0; Makefile:4367 not 3620.
• FV_SURFACE_MAP.md:21 row 9 "Imported WOTS parameters exclude C10" — the split base now pins n_val/log2_w_val/len_val as census-tracked axioms (base-c10-split/SPHINCS_PLUS.ec:43-131).
• KatVectors.lean ↔ c10_test_vectors.json sync is manual with no regenerate+diff gate; Lean KAT runs in no workflow (regeneration today: byte-identical, no live drift).
• check_c10_transcription.py positional lint reads constants/histogram out of -- comments (a deleted statement survives as a comment); the AST check backstops it today — strip comments per line to close the model gap.

Found 2026-08-20 FV red-team.

[Nicola-Ceornea]

MOSTLY FIXED in working tree. Done: AXIOM_STATUS Kontrol 4/4→7/7 (33 total) + certora artifacts marked HISTORICAL/UNEXECUTED; THE_CLAIM 30→33; PINNED_CODEHASHES/DEPLOYED_BYTECODE_PIN_CAVEAT 38→42 + 12-vector corpus; PinnedCodehashes.t.sol comment; KONTROL_SCOPING:87; checkct 4→5 drivers (STATUS×2, tooling-and-systems, Makefile comment); HW 12→14 was already 14 (map corrected with row-4 edit); TLA README 17/6; map row 9 left to the owner's easycrypt session; KatVectors regen+diff step added to ci.yml (regen is byte-identical); positional transcription lint now strips comments (comment-smuggle attack caught). REMAINING (banked): a wider '10/10' KAT-count drift across ~11 docs/lean comments not assigned to any wave (A3_1_*.md, ASSURANCE_CASE, DISCHARGE_PLAN, EUF_CMA_INCONSISTENCY, TRUST_ASSUMPTIONS, lean/Main.lean:111 etc.).