Reporting an integer_squareroot Bug in the Ethereum Consensus Specification

Challenge

The Ethereum consensus specification is the Python reference that all Ethereum consensus-layer client implementations must follow. It governs node inclusion, validation, and validator penalty processes. Errors in this specification can propagate to every conformant client and, in the worst case, lead to availability issues or other operational disruption of the consensus layer.

The specification is written in Python. While prior formal-methods work had targeted parts of the Ethereum 2.0 beacon chain, no BMC-based verifier for Python had been publicly available — the only directly comparable tool (MSV) had no public source or reproducible artefacts. There was therefore no off-the-shelf bounded model checker to apply to the eth2spec Python codebase.

Approach

Our team led the development of ESBMC-Python, the first publicly available BMC-based Python code verifier (per ISSTA 2024 paper §4). ESBMC-Python is released as part of the open-source ESBMC project. It parses Python into an AST, performs type inference (inserting AnnAssign nodes with explicit type information), and then translates Python expressions and statements into ESBMC's GOTO intermediate representation, where the existing symbolic-execution + SMT-solving pipeline applies. Properties checked include division-by-zero, arithmetic overflows, and assertion failures.

To apply ESBMC-Python to the Ethereum consensus specification (eth2spec), we extended the front-end with custom types — uint64, uint128, and uint256 — and verified each function individually with non-deterministic inputs.

The bug

def integer_squareroot(n: uint64) -> uint64:
  x = n
  y = (x + 1) // 2  # ← overflows to 0 when n = 2⁶⁴ − 1
  while y < x:
    x = y                 # x becomes 0 after the overflow
    y = (x + n // x) // 2  # ← ZeroDivisionError: n // 0
  return x

# Input:  n = 2⁶⁴ − 1 (maximum uint64 value)
# Result: ZeroDivisionError — the unsigned integer overflows to 0,
#         then is used as the denominator of a division operation.
# ESBMC-Python: confirmed the bug and produced a counterexample trace.

Results

References

1. Bruno Farias, Rafael Menezes, Eddie B. de Lima Filho, Youcheng Sun, Lucas C. Cordeiro. ESBMC-Python: A Bounded Model Checker for Python Programs. ISSTA 2024: 1836–1840. doi.org/10.1145/3650212.3685304
2. ethereum/consensus-specs PR #3600. Handle integer_squareroot bound case. Merged 15 February 2024. github.com/ethereum/consensus-specs/pull/3600