Formalizing FOCIL in Lean 4

Consensus
1

FOCIL (EIP-7805) is the censorship-resistance headliner scheduled for Hegotá. The selling point everyone repeats is “1-out-of-N honesty among IL committee members”: one non-equivocating member listing a transaction is enough to force its inclusion in the canonical block.

I wanted to know what that claim looks like under a microscope. The short answer is that it holds, derived end-to-end from Ethereum’s standard >2/3 honest-validator assumption, but writing it down in Lean surfaced three things about the spec that I think are worth discussing.

The repository is github.com/rahulbarmann/focil-lean4. It is pure Lean 4, no Mathlib, builds in tens of seconds from a stock toolchain. Five pure safety theorems are zero-axiom; the PoS-derived chain inherits propext and Quot.sound only; Classical.choice and sorryAx are not used anywhere.

The post is structured as: §1 the safety claim, §2 how the PoS lift works, §3 the three observations the formalization surfaced, §4 what is out of scope and where the natural next steps lie, §5 how to reproduce the audit, §6 questions I’d value feedback on.

1. The safety claim

The headline theorem in Focil/EndToEnd.lean:

theorem focil_concrete_pos_safety
    {s : StakeModel} (r : AttesterRun s)
    (b : Block) (tx : Transaction)
    (initial : AccountState)
    (h_canAppend_pin :
      r.canAppend = fun tx' b' => canAppendToBlock initial b' tx')
    (h_listed_by_some_honest_member :
      ∃ il, il ∈ r.state.stored_ils
            ∧ IsConsidered r.state il
            ∧ tx ∈ il.transactions)
    (h_can_append    : canAppendToBlock initial b tx)
    (h_block_not_full: ¬ r.full b)
    (h_canonical     : IsCanonical r.toForkChoice b) :
    tx ∈ b.transactions

In words: fix any StakeModel with 3H > 2N (the supermajority condition, where H is the honest-validator count and N is the total) and any AttesterRun over it whose validity predicate is the nonce-only account-state proxy. For any block b and transaction tx: if some inclusion list in the store is non-equivocating and contains tx, the block has accumulated a strict 2/3 quorum, tx's nonce matches its sender’s expected nonce in b's post-state, and b is not full, then tx \in b's transactions.

There is no opaque CanAppend here. The validity layer is a real account-state predicate, the same cheap nonce proxy that gets called out for the EOA case in soispoke’s FOCIL :handshake: Native Account Abstraction post on magicians.

The proof composes three pieces:

  1. The 1-of-N theorem focil_one_of_n_protection in Focil/Safety.lean, parameterised over the validity predicate.
  2. The PoS-derived ForkChoice lift AttesterRun.toForkChoice, which discharges both fork-choice obligations from the supermajority assumption (more on this in §2).
  3. The concrete canAppendToBlock from Focil/AccountState.lean.

The chain inside the load-bearing lemma canonical_implies_compliant is just:

b canonical \Rightarrow b has a quorum (def of canonicality) \Rightarrow \exists honest v who voted for b (quorum_has_honest_voter) \Rightarrow b is FOCIL-compliant against the bundled store (honest_attester_compliance).

The censorship-resistance result then follows by instantiating compliance at the witness IL and the candidate transaction. The compliance predicate unfolds to a three-way disjunction (tx is included, or not appendable, or block full); the latter two are excluded by hypothesis, leaving inclusion.

The overall slogan: FOCIL safety is a structural consequence of canonicality relative to a fork-choice rule that filters non-compliant blocks. The structure is what does the work; the proofs are just walking the structure.

2. The counting argument behind the PoS lift

The piece of this I find genuinely interesting is quorum_has_honest_voter. It says only that a block reaching a quorum has at least one honest voter, which is strictly weaker than the full >2/3 honest supermajority Ethereum PoS relies on. That weaker assumption is all the censorship-resistance proof needs; the supermajority is used only as an input to derive it.

Let H be the number of honest validators, V_b the number of validators who voted for b, and N the total validator count. The lift takes two inputs: 3H > 2N (the supermajority assumption) and 3V_b > 2N (a 2/3 quorum on b). Adding the inequalities:

3(H + V_b) > 4N

so H + V_b > N, hence the honest set and the voter-for-b set cannot be disjoint inside a population of N validators. The witness honest voter falls out of a counting-pigeonhole lemma:

private theorem filter_count_overlap
    {α : Type} (L : List α) (P Q : α → Bool)
    (h : L.length < (L.filter P).length + (L.filter Q).length) :
    ∃ x, x ∈ L ∧ P x = true ∧ Q x = true

Proven by induction on L with a 2 \times 2 case split on (P hd, Q hd). No Mathlib, no Classical.choice. Then AttesterRun.toForkChoice packages a stake model and an attester-run into a ForkChoice value with both obligations proven, not postulated.

The stake model is unweighted in this version (one validator counts as one stake unit). The counting argument generalises to weighted sums in the obvious way, and that’s a clean follow-on item.

There is something worth pulling out separately here. The architectural fact this exposes is that censorship resistance does not need the full BFT weight of PoS: it needs only the existence of one honest dissenting attester, and that follows from the supermajority via counting. Liveness arguments may need more; safety doesn’t.

3. Three observations from doing this

Documented at length in FINDINGS.md. The short version of each, with the question I’d want feedback on attached.

3.1 Equivocation as a censorship channel

The fork-choice changes specify that a second distinct IL from the same committee member adds them to inclusion_list_equivocators, after which all of their ILs are ignored, including the honestly-listed transactions in their first IL.

This is correct fork-choice safety. You cannot trust a Byzantine signer. But it does degrade the “1-of-N honesty” guarantee to “1-of-(N-\text{equivocators})” for any transaction that was on a single committee member’s IL, when that member is then caught equivocating. The EIP records the equivocation evidence; I have not found an explicit slashing rule attached to it in the EIP body, though I’d be happy to be pointed at one.

The Lean model captures this exactly: IsConsidered state il becomes false once the author is in state.equivocators, so the safety theorem’s hypothesis fails for that IL. The theorem still goes through for any other honest IL listing tx. Scenarios 9 and 10 in Tests/Examples.lean walk through the concrete state.

The question is how the spec authors think about this. Is it an acceptable bandwidth-level cost (one validator’s stake at risk to void one committee seat’s contribution for one transaction), or should the equivocation evidence carry an explicit slashing penalty? Either is reasonable; the spec text doesn’t currently commit to one interpretation.

3.2 Adversarial validity changes

EIP-7805’s payload-construction discussion notes that a proposer can legitimately omit an IL transaction tx if tx is no longer valid at block-production time. A malicious proposer would like to engineer that invalidity right before they build the block.

Nonce front-running is the simplest attack: a colluding party submits a transaction with the same sender as the IL transaction, the proposer appends it, and the IL transaction’s nonce is now stale. The proposer can then invoke the conditional-inclusion exemption.

This is formalised as front_running_breaks_appendability:

theorem front_running_breaks_appendability
    (initial : AccountState) (b : Block)
    (tx_il tx_evil : Transaction)
    (h_same_sender    : tx_evil.sender = tx_il.sender)
    (h_il_appendable  : canAppendToBlock initial b tx_il)
    (h_evil_appendable: canAppendToBlock initial b tx_evil) :
    ¬ canAppendToBlock initial
        { b with transactions := b.transactions ++ [tx_evil] }
        tx_il

A small thing worth noting: I do not need to assume the two transactions share a nonce explicitly. Same sender plus simultaneous appendability already forces nonce collision (both must equal the sender’s expected nonce in the post-state). That’s the minimal hypothesis set.

Scenario 13 fires this on real data: sender 100, nonce 0 for both transactions; the proposer extends an empty block with the colluding tx; the IL tx is no longer appendable.

The current concrete model tracks per-sender nonces only. A balance-aware variant capturing the balance-drain attack is structurally the same proof shape with a doubled case surface; this is a natural next contribution.

The cost of the attack is one gas-fee payment with no slashing (the attacker is transacting, not equivocating). The question for the spec authors: does the EIP commit to a per-account-state abstraction the proposer must respect (snapshot pre-state before any same-slot transaction the proposer includes in their block), or is the gas cost considered a sufficient deterrent for the EOA case? Both are reasonable. I haven’t found a definitive position in the EIP body or the magicians thread.

3.3 The honest-attester invariant must be relativized to the attester’s local store

The fork-choice changes specify, in English, that honest attesters refuse to vote for FOCIL-non-compliant blocks. Natural enough.

When I tried to write that as a Lean predicate, I noticed the rule has two non-equivalent formal readings depending on how the fork-choice store is quantified:

  1. Globally quantified. For every conceivable fork-choice store, honest attesters who voted for b make b compliant against that store.
  2. Locally relativized. Honest attesters who voted for b make b compliant against the store they themselves observed at attestation time.

Reading (1) is unsatisfiable non-vacuously when EVM validity is opaque. Pick any tx \notin b's transactions, consider the adversarial store whose only stored IL contains tx. Compliance becomes a three-way disjunction whose disjuncts are not dischargeable for arbitrary b. The only escape is to make the antecedent unsatisfiable by emptying the vote relation, which voids the rule.

Reading (2) is the satisfiable one, and it matches what an honest attester actually does: vote relative to their fork-choice store at attestation time, not relative to all conceivable stores. The EIP is correct under reading (2). My concern is just that any informal proof sketch composing the rule across attesters with different store snapshots, treating it as a single global invariant, has a hidden quantifier-scope assumption that the English-prose version does not surface.

The fix in the Lean model is small and structural: the ForkChoice structure bundles the store and fullness model as fields, fixing reading (2) at the type level. The corrected formalisation admits a non-vacuous concrete instance (threeValidatorForkChoice in Tests/Examples.lean), where both soundness obligations are discharged by genuine case analysis, and the PoS lift in §2 does the same starting from the supermajority.

I think this is the kind of subtle assumption a Lean formalisation is genuinely good at surfacing. Curious whether others read the rule the same way or differently.

4. Out of scope, and the natural next steps

Worth being precise about. Each item below is named in the codebase as a candidate seam for follow-on work; the order is roughly the order I’d take them in.

  • Sequential validity dependence between IL transactions. EIP-7805’s payload-construction notes that an IL transaction can become valid because an earlier IL transaction was appended; the current CompliantWith predicate quantifies per-transaction independently against the final block. Capturing this is the highest-leverage open item. Structurally invasive: the validity predicate would need to take a list of “tentatively appended transactions” as a parameter, and the case analysis in the safety proof would change shape.
  • Balance-aware concrete validity. The current concrete model tracks per-sender nonces only. A balance-aware variant would let me formalise the balance-drain attack (§3.2) end-to-end against the same PoS-derived chain. Same proof shape; the case surface roughly doubles.
  • EIP-8141 Frame Transactions. Would need to formalise the bounded validation-prefix replay rule from the FOCIL :handshake: Native Account Abstraction thread. Bigger scope; better as a separate piece of work.
  • Equivocator detection. state.equivocators is taken as input. Modelling on_inclusion_list and proving it correctly populates the equivocator set would close the input-vs-derived gap.
  • IL gossip / network model. Network adversaries that selectively delay IL propagation reduce the effective committee size. Currently captured only as a precondition (il ∈ state.stored_ils).
  • Stake weighting. Each validator counts as one unit; the counting argument generalises to weighted sums. Routine.
  • Liveness. This is a safety-only formalisation. A liveness companion (a compliant block always exists at every slot) is a separate research direction.

5. Reproducing the audit

Five pure safety theorems are zero-axiom. The PoS-derived chain inherits propext and Quot.sound via omega and simp on List.length lemmas; nothing else.

To check this yourself:

cat > AuditAxioms.lean <<'EOF'
import FocilLean4

#print axioms Focil.focil_one_of_n_protection
#print axioms Focil.focil_censorship_resistance
#print axioms Focil.censoring_block_not_canonical
#print axioms Focil.canonical_implies_compliant
#print axioms Focil.focil_concrete_safety
#print axioms Focil.focil_concrete_pos_safety
#print axioms Focil.focil_concrete_pos_censoring_block_not_canonical
EOF
lake env lean AuditAxioms.lean

The five pure theorems should report does not depend on any axioms; the PoS/concrete chain reports [propext, Quot.sound]. The build is Mathlib-free; lean-toolchain pins Lean 4.29.1; cold-cache build is on the order of tens of seconds.

6. Questions I’d value feedback on

Roughly in order of importance:

  • §3.1 (equivocation as a censorship channel): is this an acceptable trade-off as written, or an item the spec should attach a slashing rule to?
  • §3.2 (adversarial validity changes): is this a known concern with a settled position elsewhere I haven’t found?
  • §3.3 (the quantifier-scope subtlety): does this read as substantive to others, or as a stylistic artifact of the way I chose to model the fork-choice rule?

Beyond those, the most useful contribution opportunity in my read is the first item in §4: refining CompliantWith to capture sequential dependence.

License is CC0-1.0, matching the EIPs. Happy to discuss any of the above either here or as GitHub issues.