FOCIL (EIP-7805) promises 1-of-N honesty among IL committee members: one non-equivocating member is enough to force a tx into the canonical block. I formalized that claim in Lean 4. It holds, derived end-to-end from Ethereum's standard >2/3 honest-stake assumption. No opaque validity predicate in the safety chain. The concrete EVM-validity layer is the nonce proxy @soispoke describes for the EOA case. Five pure safety theorems are zero-axiom. The PoS-derived chain inherits propext and Quot.sound only. Three observations from doing this: 1. Equivocation is a free censorship channel for any tx listed by only one committee member. A Byzantine member can void their own contribution by signing two distinct ILs. 1-of-N degrades to 1-of-(N − equivocators). 2. Adversarial validity. A colluding party submits a tx from the same sender as the IL tx; the proposer appends it; the IL tx is now stale and legitimately omittable. Formalized as a theorem on a concrete account-state model. Cost: one gas fee, no slashing. 3. The honest-attester invariant has two non-equivalent formal readings. The natural global reading is unsatisfiable non-vacuously when EVM validity is opaque; the spec needs the locally-relativized reading. The English-prose version doesn't surface this.

I published a production implementation of OpenAC as an npm package. @l8zk/sdk generates and verifies Spartan2 zero-knowledge proofs with performance matching the paper: • ~96ms show proof • ~34ms verification • full reblinding for unlinkability • transparent setup (no trusted ceremony) Current scope: pre-compiled circuits with fixed payload size, matching official PSE benchmarks. Dynamic credential support is under active development. Built on top of the MIT-licensed zkID work by the PSE / Ethereum Foundation team.