The Signal: Ethereum — A Formal Analysis

This documentation provides the complete formal analysis for the TSEth consensus core. It is split into two primary parts, which are best read in order:

1. Formalization of the Consensus Algorithm

   • This document formally defines the Atomic Finalization algorithm, its data structures, and proves its compatibility with the standard Casper FFG.

2. Safety Analysis of Balance Drift

   • This document provides the detailed mathematical derivation of the safety margin required to account for validator balance drift when verifying proofs from a historical state.

Introduction and Framework

TSEth is a zkVM-friendly implementation of Casper FFG, designed around a simplified Atomic Finalization algorithm. The core of this approach is to verify a state transition from a given consensus state—derived from a previously finalized checkpoint—to a new, target consensus state. This verification is performed within a zkVM guest program, allowing a full node to generate a succinct proof of finality.

This process is initiated by providing the guest program with a consensus state containing a finalized checkpoint. The root of this checkpoint serves as a root of trust, allowing any data from the corresponding Beacon state (like the validator registry) to be proven via Merkle proofs and used as trusted inputs for the guest.

To prove this state transition, the guest program also requires information not contained in the trusted state. The prover must supply a witness that includes the sequence of supermajority links leading to the new finality, as well as auxiliary data like future RANDAO values for committee calculation.

The fundamental challenge is that the guest program must use the validator balances from the trusted state at $epoch_0$ to validate these attestations. This creates a discrepancy with the official Ethereum protocol, which uses the effective balances from the epoch in which the justification is applied. This balance drift grows with the number of epochs between the trusted checkpoint and the new target.

This body of work provides a formal safety analysis for this balance drift. We derive a conservative upper bound for this drift and use it to define a safety margin ($\delta$). By requiring the attesting balance in our guest program to exceed the standard two-thirds supermajority by this margin, we can guarantee the safety of the finalized checkpoint, even without access to the most recent state.

Formalization of the Consensus Algorithm

Definition: Consensus State

Given two checkpoints $f$ and $c$, where $f$ is also called the finalized checkpoint and $c$ the current justified checkpoint. We call the ordered pair $(f,c)$ a Consensus State, when $f$ is a predecessor of $c$.

Algorithm: Atomic Finalization

Input:

• A consensus state $(f,c)$.
• A sequence of $k$ supermajority links $\left(c\to b_1,b_1 \to b_2, \dots, b_{k-1} \to b_k \right)$.

Procedure:

The algorithm proceeds only if the final link in the sequence, $b_{k-1} \to b_k$, satisfies the condition $epoch(b_k) = epoch(b_{k-1}) + 1$. Otherwise, the operation aborts.

Output:

• The new consensus state $(b_{k-1}, b_k)$

Compatibility Analysis with Casper FFG

We argue the compatibility of our Consensus Algorithm with Casper FFG, assuming no 2-finalizations occur. The finalized_checkpoint and current_justified_checkpoint fields in the Beacon state induce a valid consensus state.

Definition: Induced Consensus State

We call a consensus state $(f,c)$ induced by the Beacon state at checkpoint $s$, when $f$ matches the finalized_checkpoint field and $c$ matches the current_justified_checkpoint field of the Beacon state as referenced by the checkpoint $s$.

Theorem 1

Let $s$ and $t$ be two finalized checkpoints in a view $G$ of Casper FFG, where $s$ is a predecessor of $t$. Let $\mathcal{A}$ be the chain of supermajority links ("attestations") included in the blocks between $s$ and $t$ that cause $t$ to be finalized. Executing the Atomic Finalization algorithm with the consensus state $(f,c)$ induced by $s$ and the chain of supermajority links ("attestations") included in the blocks between $s$ and $t$, will return the consensus state induced by $t$.

Proof:

By definition, for Casper FFG to finalize a checkpoint $t$, there must exist a supermajority link from a justified checkpoint $t'$ to $t$, where $epoch(t) = epoch(t') + 1$. The sequence of attestations $\mathcal{A}$ represents the chain of justifications leading to this final link. Our algorithm's procedural check, $epoch(b_k) - epoch(b_{k-1}) = 1$, directly mirrors this requirement. The algorithm's output $(b_{k-1}, b_k)$ therefore corresponds to $(t', t)$, which is precisely the new (finalized_checkpoint, current_justified_checkpoint) state in Casper FFG.∎

This shows that our consensus algorithm will always be able to follow the Beacon chain's consensus, as long as there are no cases of 2-finality.

Theorem 2

Let $s$ be a finalized checkpoint in a view $G$ of Casper FFG. Let $(f',c')$ denote the output of our algorithm when executed with the consensus state induced by $s$ and a valid set of supermajority links as input. Under the accountable safety assumption ($< \frac{1}{3}$ of the validators by weight violate a slashing condition), $f'$ will also be finalized for $G$.

Proof Sketch:

This follows directly from Casper FFG's guarantee against finalizing conflicting checkpoints. Assume for contradiction that our algorithm finalizes $f'$ but $G$ does not. This would require $G$ to justify a pair of checkpoints $(a_m, a_{m+1})$ that "surround" the supermajority link $f' \to c'$ that our algorithm used.

The existence of both the link $f' \to c'$ and a surrounding link $a_m \to a_{m+1}$ is a slashable "surround vote" offense. Therefore, a supermajority of honest validators would never create this situation. Any valid view $G$ must respect the finalization of $f'$. ∎

While $f'$ is safe, $c'$ is only justified. Due to malicious behavior or network latency issues, a failure to justify $c'$ in $G$ is theoretically possible and would represent a liveness fault, not a safety violation.

A Note on 2-Finality

This algorithm deliberately excludes cases of 2-finality, as they introduce significant complexity to our atomic, single-chain model.

The core challenge lies with finalization rules such as a supermajority link $b_{n-2} \to b_n$, which finalizes $b_{n-2}$. For this rule to be valid, both $b_{n-2}$ and $b_{n-1}$ must be justified. Our algorithm is designed to process one continuous chain of justifications from a single starting checkpoint ($c$), whereas a 2-finality rule would require verifying two distinct justification chains.

One might think the Beacon state's previous_justified_checkpoint and current_justified_checkpoint fields could serve as these two required checkpoints. However, this is not a reliable solution. The previous_justified_checkpoint field is defined as the current_justified_checkpoint of the previous epoch. This can lead to situations with an intermediate justified checkpoint that isn't captured by either field. For example, previous_justified_checkpoint could be $B_2$ and current_justified_checkpoint could become $B_4$, while $B_3$ was justified in the interim (Case 1 and Case 3 of Fig. 8. in Combining GHOST and Casper).

Fortunately, the FFG version implemented in the Ethereum Beacon Chain introduces practical constraints that simplify this problem. By only considering the justification status of the last four epochs and imposing other timing conditions, it prevents the most complex theoretical 2-finality scenarios from occurring. This ensures the conditions can be verified without needing a more complex algorithm that takes multiple justification chains as input.

Nevertheless, adapting our clean, single-chain model to formally handle even these simplified 2-finality rules would add considerable complexity. We therefore leave this extension for a future revision.

Safety Analysis of Balance Drift

The Safety Margin Formula

Key Variables and Notation

Let the trusted, finalized checkpoint be denoted by the pair $(f_0, epoch_0)$, and the target checkpoint whose finality is being proven be $(f_n, epoch_n)$. The number of elapsed epochs is $n = epoch_n - epoch_0$. We define the following:

• Validator Sets:

  • $V_0$: The set of active validators at $epoch_0$.
  • $V_n$: The set of active validators at $epoch_n$.
  • $A_n \subseteq V_n$: The subset of validators that have attested to the supermajority link required to justify $epoch_n$.

• Total Active Balance:

  • $\hat{B}_0$: The total effective balance of all validators in $V_0$, measured at $epoch_0$. This is the value get_total_active_balance would return at $epoch_0$.
  • $\hat{B}_n$: The total effective balance of all validators in $V_n$, measured at $epoch_n$.

• Attesting Weight:

  • $w_0(A_n)$: The sum of the effective balances of the validators in $A_n$, as measured from the trusted state at $epoch_0$. This is the value our zkVM guest program calculates.
  • $w_n(A_n)$: The sum of the effective balances of the validators in $A_n$, as measured by the canonical protocol at $epoch_n$. This is the value we are trying to safely reason about.

Derivation

The canonical requirement for finality is that the attesting weight at $epoch_n$ meets the two-thirds threshold: $$w_n(\mathcal{A}_n) \ge \frac{2}{3} \hat{B}_n$$

To create a bound verifiable from the trusted state at $epoch_0$, we must account for the maximum possible "balance drift". As slashings that occur after $epoch_0$ cannot be known from the trusted state, the total balance of these slashed validators must be provided as a separate input, $S$. We then define:

• A: The maximum possible increase in the effective balance of the non-attesting validators ($V_n \setminus A_n$) between $epoch_0$ and $epoch_n$.
• E: The maximum possible decrease in the effective balance of the attesting validators ($A_n$) between $epoch_0$ and $epoch_n$.
• S: The total effective balance of validators slashed between $epoch_0$ and $epoch_n$. While slashed validators are penalized, their balance still contributes to the total active balance ($\hat{B}_n$) for the supermajority calculation, but they are excluded from the attesting weight ($w_n$).

The safety condition, as viewed from $epoch_0$, can be expressed as: $$w_0(\mathcal{A}_n) - E - S \ge \frac{2}{3} (\hat{B}_0 + A - E)$$

Rearranging this to solve for the required attesting weight $w_0(A_n)$ gives us our safety margin, $\delta$: $$w_0(\mathcal{A}_n) \ge \frac{2}{3} \hat{B}_0 + \frac{1}{3}(2A + E) + S$$ Thus, the safety margin is: $$\delta = \frac{1}{3}(2A + E) + S$$

Unless otherwise stated, every $A$- or $E$-sub-term, and therefore $\delta$, itself is expressed in ETH. When a term is derived from a raw validator count we implicitly multiply by 1 ETH per validator.

Bounding Balance Fluctuation Sources

We now derive conservative upper bounds for $A$ and $E$ over $n$ epochs, based on the Ethereum Electra specification.

Validator Churn and Consolidations

• Activations: In the current model, the set of validators that can become active during the lookahead period $n$ is completely determined by the trusted state at $epoch_0$. A validator's activation requires that its activation_eligibility_epoch is less than or equal to the finalized_checkpoint.epoch.¹ Since the finalized_checkpoint is fixed at $epoch_0$ for the entire verification process, any validator not already in the activation pipeline at $epoch_0$ cannot become active. Therefore, the increase in attesting weight from these known activations can be calculated precisely by the guest and is not a source of unbounded drift.
• Exits & Consolidations: For the zkVM guest to compute correct committee shuffles, it must account for any validator exits or consolidations that occur after the trusted checkpoint. This information is provided as part of the untrusted witness data. From the perspective of the validator registry, a voluntary exit and a consolidation are indistinguishable. To create a single, safe upper bound for balance churn, their respective churn limits must be combined. This combined value corresponds to the get_balance_churn_limit in the specification, which is based on the constant CHURN_LIMIT_QUOTIENT (65536). The official specification calculates this dynamic churn limit against the current total active balance at any given epoch $k$, with a floor of MIN_PER_EPOCH_CHURN_LIMIT_ELECTRA (128 ETH). To prevent a malicious prover from supplying fraudulent data, the guest program validates the witness against a hardcoded churn limit. Simply using a limit based on $\hat{B}_0$ could be unsafe, as the total active balance might increase over $n$ epochs, thus increasing the real churn limit. To account for this potential growth, the implementation uses a conservative factor of two. While a full formal analysis of this factor is complex, it serves as a safe, static bound for a reasonably small lookahead period $n$. Because the guest strictly enforces this specific check, our formal analysis must adopt the exact same bound:
  • $A_{churn} \le n \cdot 2 \cdot \max(128, \hat{B}_0 / 65536)$
  • $E_{churn} \le n \cdot 2 \cdot \max(128, \hat{B}_0 / 65536)$

Rewards and Penalties

The total issuance per epoch is a function of the total active balance, $\hat{B}$ in Gwei. It is a well-known design choice that per epoch the total issuance is $$\hat{B} \cdot \frac{\mathtt{BASE_REWARD_FACTOR}}{\sqrt{\hat{B}}} = 64\sqrt{\hat{B}},\text{Gwei}$$ Even with a total active balance as high as 100 million ETH, the total issuance would be only a little over 20 ETH. For simplicity and to be highly conservative, we use a constant upper bound of 48 ETH per epoch for both rewards and penalties. This is more than enough to account for future balance increases or "catch up" rewards for missed attestations due to skipped slots in the previous epoch

• Rewards (contributing to A): $A_{rewards} \le 48n$
• Penalties (contributing to E): $E_{penalties} \le 48n$

Inactivity Leak Penalty

During a prolonged non-finality event (an "inactivity leak"), inactive validators are penalized with increasing severity. The penalty over $n$ epochs for validator $i$ with effective balance $B^i$ is $\sum_{k=4}^n \frac{B^i}{2^{24}}k$.² This quadratic penalty growth is a key feature of the inactivity leak.

To derive a conservative upper bound for this penalty's contribution to $E$, we make the following worst-case assumptions:

1. All attesting validators in our set ($A_n$) are considered inactive from the beginning of the period.
2. The inactivity leak starts at the first epoch, i.e. we are not considering MIN_EPOCHS_TO_INACTIVITY_PENALTY.
3. The total balance of these attesting validators is bounded by the total active balance of the entire network, $\hat{B}_n$.

$$E_{inactivity} \le \left(\sum_{i \in \mathcal{A}_n} B^i\right) \cdot \frac{n(n+1)}{2 \cdot 2^{24}} \le \frac{\hat{B}_n \cdot n(n+1)}{33554432}$$

Slashing

The slashing penalty has two parts: an initial penalty and a larger correlation penalty.

• Initial Penalty: This penalty is immediately applied but does not change the total active balance $\hat{B}_n$ (it's redistributed). Its primary effect is that the slashed validator's weight is removed from the attesting set $A_n$ (even though they may still attest), which is already captured by the term $S$ in our formula.
• Correlation Penalty: This is applied much later, after the validator is already withdrawable and thus no longer part of the active set. It can be ignored for this analysis.

Hysteresis

The protocol updates a validator’s effective_balance only when the actual balance crosses a hysteresis band.³ This creates two distinct sources of drift we must account for: a baseline drift from ordinary rewards and a large, event-driven jump from EIP-7251.

1. Baseline Hysteresis Drift: For any validator, ordinary rewards and penalties can cause their balance to cross a threshold, changing their effective_balance by at most 1 ETH. This creates a baseline drift potential for every validator in the set.
2. EIP-7251 Compounding Switch: With EIP-7251, a validator can submit a ConsolidationRequest to switch to compounding credentials, raising their maximum effective balance from MIN_ACTIVATION_BALANCE (32 ETH) to MAX_EFFECTIVE_BALANCE_ELECTRA (2048 ETH). This can trigger a one-time jump of up to 2016 ETH. However, the number of these "switch" events is strictly limited by the protocol. The BeaconBlockBody can contain at most MAX_CONSOLIDATION_REQUESTS_PER_PAYLOAD (2) per block. With 32 slots per epoch, a maximum of 64 switches can be processed per epoch.

To construct our final bound, we combine these two effects. We assume the worst case where all 64n possible switches occur and all benefit non-attesting validators. Each switch contributes an additional 2015 ETH of drift on top of the 1 ETH baseline drift already accounted for.

• $A_{hysteresis} \le \underbrace{|V_n \setminus \mathcal{A}$n|}{\text{Baseline Drift}} + \underbrace{(2015 \cdot 64n)}_{\text{EIP-7251 Jumps}} = |V_n \setminus \mathcal{A}_n| + 128960n
• $E_{hysteresis} \le |\mathcal{A}_n|$ (The decrease remains bounded by the 1 ETH baseline drift)

From Formal Model to Implemented Parameter

While this document derives a dynamic safety margin, $\delta$, the implementation employs a simplified, fixed supermajority threshold. For instance, the default configuration requires a justification of 85% (justification_threshold_factor: 85, justification_threshold_quotient: 100).

This fixed threshold is not an alternative to the $\delta$ analysis; it is a practical parameter chosen based on it. The formal derivation of $\delta$ allows us to calculate the worst-case balance drift for the configured epoch_lookahead_limit. The implemented 85% threshold is a conservative value chosen to exceed $2/3 + \delta$ for all permissible lookahead scenarios, thereby guaranteeing safety without requiring the zkVM guest to perform the complex $\delta$ calculation at runtime. The formal analysis thus serves as the fundamental justification for the safety of the implemented fixed threshold.

Bounding the Total Safety Margin

By combining the individual components for the maximum possible increase in non-attesting weight ($A$) and the maximum decrease in attesting weight ($E$), we get the following bounds: $$\begin{align*} A &= A_{\text{churn}} + A_{\text{rewards}} + A_{\text{hysteresis}} \ &\leq 2n\max(128,\frac{\hat{B}_0}{65536}) + 48n + |\mathcal{V}_n \setminus \mathcal{A}_n| + 128960n \end{align*}$$

$$\begin{align*} E &= E_{\text{churn}} + E_{\text{penalties}} + E_{\text{inactivity}} + E_{\text{hysteresis}} \ &\leq 2n\max(128,\frac{\hat{B}_0}{65536}) + 48n + \frac{\hat{B}_n n(n+1)}{33554432} + |\mathcal{A}_n| \end{align*}$$ Substituting these into the safety margin formula, $\delta = \frac{1}{3}(2A + E) + S$, yields the final comprehensive bound: $$\delta \le 48n + 2n\max(128,\frac{\hat{B}_0}{65536}) + \frac{\hat{B}_n n(n+1)}{100663296} + \frac{2}{3}|\mathcal{V}_n| + 85974n + S$$

To make this formula computable, we replace the unknown values at epoch $n$ with conservative upper bounds derived from the trusted state at $epoch_0$. While the balance from validators activating during the lookahead period can be calculated precisely, it is simpler for the purpose of this meta-analysis to use a conservative upper bound. The upper bound for the total active balance $\hat{B}_n$ is thus composed of the initial balance, a bound on balance from new activations (MAX_PER_EPOCH_ACTIVATION_EXIT_CHURN_LIMIT), the maximum rewards, and the maximum hysteresis drift:

$$\hat{B}$$n \le \hat{B}0 + \underbrace{(256 \cdot n)}{\text{queued activations}} + \underbrace{(48 \cdot n)}{\text{rewards}} + \underbrace{(|V_0|+128960\cdot n)}_{\text{hysteresis}}

Similarly, the upper bound for the number of validators is:

$$|V_n| \le |V_0| + (8 \cdot n)$$

The resulting safety margin $\delta$ can be calculated programmatically as shown in the Python implementation below.

def calculate_delta(B_0: int, V_0: int, S: int, n: int) -> int:
    """
    Calculates a conservative safety margin delta for TSEth.

    Args:
        B_0: Total active effective balance at the trusted epoch (in ETH).
        V_0: Number of active validators at the trusted epoch.
        S: Total slashed balance since the trusted epoch (in ETH).
        n: Number of epochs to look ahead.
    """
    # An upper bound for the total active balance at the target epoch
    # +V_0  (≤1 ETH hysteresis jump per validator)
    B_n = B_0 + (256 * n) + (48 * n) + V_0 + 128960 * n
    # An upper bound for the active validators at the target epoch
    V_n = V_0 + (8 * n)

    churn_term = n * 2 * max(128, B_0 / 65536)
    reward_term = 48 * n
    inactivity_term = (B_n * n * (n + 1)) / 100663296
    hysteresis_term = 2 * (V_n + 128960 * n) / 3

    delta = reward_term + churn_term + inactivity_term + hysteresis_term + S

    # Return the final margin, rounded up for a conservative estimate.
    return math.ceil(delta)

Conclusion

This analysis provides a self-contained, conservative bound for the safety margin $\delta$, depending only on the initial state at $epoch_0$, the slashed balance $S$, and the lookahead period $n$. The model's robustness is best illustrated by examining its sensitivity to these parameters.

With the current TSEth default configuration requiring ≥85% voting participation and a finalization lookahead of at most 10 epochs, the system maintains strong security guarantees. For instance, using Ethereum mainnet data from July 2025 (35,475,927 ETH staked by 1,087,747 active validators), TSEth can safely finalize checkpoints even if validators with a combined effective balance of over 4.9 million ETH were slashed.

The safety margin is most sensitive to the lookahead period, $n$. While a short lookahead results in a modest $\delta$, the margin grows quadratically as $n$ increases due to the inactivity leak term, demonstrating the importance of the configured epoch_lookahead_limit. Similarly, the model correctly scales with the total slashed balance, $S$, ensuring that large-scale slashing events are safely accounted for. This framework provides a transparent and verifiable method for ensuring the safety of a ZKVM-based FFG implementation.