-
Notifications
You must be signed in to change notification settings - Fork 3
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
[FINDING] Post-remediation residual sweep: A2-demotion doc stragglers, wider 10/10 KAT-count drift, and three micro gate/doc items
findingAdversarial-review finding; evidence in docs/security/adversarial-review/findings/Adversarial-review finding; evidence in docs/security/adversarial-review/findings/priority:lowNice to have / infrastructureNice to have / infrastructuresurface:docsAttack surface / subsystem: docsAttack surface / subsystem: docsStatus: Open.#682 In EthereumPhone/PQ1;[FINDING] EasyCrypt suspicion: admitted MM45 lemma nhchwcoll_hchwpre_msg is consumed at base-c10-split/WOTS_TW_ES.ec:6542 — 'capstone dependency chain is admit-free' is an unchecked sentence
findingAdversarial-review finding; evidence in docs/security/adversarial-review/findings/Adversarial-review finding; evidence in docs/security/adversarial-review/findings/priority:mediumDefense-in-depthDefense-in-depthsurface:fvAttack surface / subsystem: fvAttack surface / subsystem: fvStatus: Open.#681 In EthereumPhone/PQ1;[FINDING] No fuzz target for the EIP-712 decode parsers (cowswap/safe binding legs); render path is covered but decode is not
findingAdversarial-review finding; evidence in docs/security/adversarial-review/findings/Adversarial-review finding; evidence in docs/security/adversarial-review/findings/priority:mediumDefense-in-depthDefense-in-depthsurface:clear-signingAttack surface / subsystem: clear-signingAttack surface / subsystem: clear-signingsurface:fvAttack surface / subsystem: fvAttack surface / subsystem: fvStatus: Open.#680 In EthereumPhone/PQ1;[FINDING] lean4checker: the 59th Lean module (Crypto/Quantitative.lean, 2026-07-26) has never had an exact-HEAD kernel replay
findingAdversarial-review finding; evidence in docs/security/adversarial-review/findings/Adversarial-review finding; evidence in docs/security/adversarial-review/findings/priority:lowNice to have / infrastructureNice to have / infrastructuresurface:fvAttack surface / subsystem: fvAttack surface / subsystem: fvStatus: Open.#679 In EthereumPhone/PQ1;[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)
findingAdversarial-review finding; evidence in docs/security/adversarial-review/findings/Adversarial-review finding; evidence in docs/security/adversarial-review/findings/priority:lowNice to have / infrastructureNice to have / infrastructuresurface:docsAttack surface / subsystem: docsAttack surface / subsystem: docsStatus: Open.#678 In EthereumPhone/PQ1;[FINDING] Kani evidence hygiene: 3 ERC-7730 Phase-D harnesses lack in-tree receipts; '173 active' overstates the enforced set by 3; map row 4 billing-outage claim stale
findingAdversarial-review finding; evidence in docs/security/adversarial-review/findings/Adversarial-review finding; evidence in docs/security/adversarial-review/findings/priority:lowNice to have / infrastructureNice to have / infrastructuresurface:fvAttack surface / subsystem: fvAttack surface / subsystem: fvStatus: Open.#677 In EthereumPhone/PQ1;[FINDING] extracted/ closure gate accepts an arbitrary project axiom outside the 66 dumped headlines — add a project-wide axiom census
findingAdversarial-review finding; evidence in docs/security/adversarial-review/findings/Adversarial-review finding; evidence in docs/security/adversarial-review/findings/priority:lowNice to have / infrastructureNice to have / infrastructuresurface:fvAttack surface / subsystem: fvAttack surface / subsystem: fvStatus: Open.#676 In EthereumPhone/PQ1;[FINDING] lint_fv (b) BreaksHash eliminator bypass + (e) paren/arrow True-conclusion evasion
findingAdversarial-review finding; evidence in docs/security/adversarial-review/findings/Adversarial-review finding; evidence in docs/security/adversarial-review/findings/priority:lowNice to have / infrastructureNice to have / infrastructuresurface:fvAttack surface / subsystem: fvAttack surface / subsystem: fvStatus: Open.#675 In EthereumPhone/PQ1;[FINDING] A2 entrypoint_honest is provable kernel-only — demote to theorem; '9 genuine premises' marketing counts a zero-information premise
findingAdversarial-review finding; evidence in docs/security/adversarial-review/findings/Adversarial-review finding; evidence in docs/security/adversarial-review/findings/priority:lowNice to have / infrastructureNice to have / infrastructuresurface:fvAttack surface / subsystem: fvAttack surface / subsystem: fvStatus: Open.#674 In EthereumPhone/PQ1;[FINDING] contracts/verity zero-sorry gate fail-open on multiline grep (12 live sorries PASS); census wrong (3 axioms, not 2); uncensused CREATE2 axiom
findingAdversarial-review finding; evidence in docs/security/adversarial-review/findings/Adversarial-review finding; evidence in docs/security/adversarial-review/findings/priority:mediumDefense-in-depthDefense-in-depthsurface:fvAttack surface / subsystem: fvAttack surface / subsystem: fvStatus: Open.#673 In EthereumPhone/PQ1;[FINDING] Deploy-profile codehash pins + DeployedBytecodeReproCheck run in no workflow — production drift is CI-invisible
findingAdversarial-review finding; evidence in docs/security/adversarial-review/findings/Adversarial-review finding; evidence in docs/security/adversarial-review/findings/priority:mediumDefense-in-depthDefense-in-depthsurface:contractsAttack surface / subsystem: contractsAttack surface / subsystem: contractssurface:onchainAttack surface / subsystem: onchainAttack surface / subsystem: onchainStatus: Open.#672 In EthereumPhone/PQ1;[FINDING] policy_cap_fence Q1 isolation check bypassed by a multi-line require (fence self-correction incomplete)
findingAdversarial-review finding; evidence in docs/security/adversarial-review/findings/Adversarial-review finding; evidence in docs/security/adversarial-review/findings/priority:mediumDefense-in-depthDefense-in-depthsurface:fvAttack surface / subsystem: fvAttack surface / subsystem: fvStatus: Open.#671 In EthereumPhone/PQ1;