Surface: fv · Severity: medium · Evidence: PoC (executed gate-logic replay + comment-stripped census) · Target: f91aa82
Claimed: contracts/verity/Makefile:45-50 "zero-sorry gate"; Verifier/Top.lean:192 census "~40 closed theorems + 2 axioms + 1 documented sorry"; the tree is named in AXIOM_STATUS.json as the deductive A3.1 closure path.
Defects:
grep -c over 13 files yields per-file path:count lines; [ "$SORRY_COUNT" -gt 0 ] errors "integer expression expected" and the if takes the false branch → gate prints PASS with 12 live sorries (Theorems.lean ×11 incl. def Reachable : Storage → Prop := sorry, Merkle.lean ×1). The sorry$ pattern also misses line 297 (trailing comment). No workflow invokes verity's ci at all.- Census is wrong: axioms are 3 —
Verifier/Hash.lean:40,47 plus PQSmartWalletFactory.lean:65 axiom predict_matches_create : (createDeterministicERC1967 …).fst = predictDeterministicAddressERC1967 … — a content-bearing CREATE2 address-prediction claim documented in verity's own TRUST_ASSUMPTIONS but in no census gate and no ledger. Two review waves on 2026-08-11 re-counted and still undercounted both numbers.
Fix: aggregate the count (awk '{s+=$2}') or reuse the comment-stripped census; correct the Top.lean census; add the factory axiom to the trust inventory; extend the axiom/sorry census to contracts/verity. Found 2026-08-20 FV red-team.
Surface: fv · Severity: medium · Evidence: PoC (executed gate-logic replay + comment-stripped census) · Target: f91aa82
Claimed:
contracts/verity/Makefile:45-50"zero-sorry gate";Verifier/Top.lean:192census "~40 closed theorems + 2 axioms + 1 documented sorry"; the tree is named inAXIOM_STATUS.jsonas the deductive A3.1 closure path.Defects:
grep -cover 13 files yields per-filepath:countlines;[ "$SORRY_COUNT" -gt 0 ]errors "integer expression expected" and theiftakes the false branch → gate prints PASS with 12 live sorries (Theorems.lean ×11 incl.def Reachable : Storage → Prop := sorry, Merkle.lean ×1). Thesorry$pattern also misses line 297 (trailing comment). No workflow invokes verity'sciat all.Verifier/Hash.lean:40,47plusPQSmartWalletFactory.lean:65axiom predict_matches_create : (createDeterministicERC1967 …).fst = predictDeterministicAddressERC1967 …— a content-bearing CREATE2 address-prediction claim documented in verity's own TRUST_ASSUMPTIONS but in no census gate and no ledger. Two review waves on 2026-08-11 re-counted and still undercounted both numbers.Fix: aggregate the count (
awk '{s+=$2}') or reuse the comment-stripped census; correct the Top.lean census; add the factory axiom to the trust inventory; extend the axiom/sorry census to contracts/verity. Found 2026-08-20 FV red-team.