Skip to content
SeamCert

Compiles is not the same as proves.

Saturday 7 November 2026 · Lean 4 statement checks · Est. 2026

← Claims ledger · Reported · Not yet replayed by SeamCert

Claims Dispatch · Sources Checked 7 November 2026

ethereum / EthLib: EIP-7951 P256VERIFY Precompile (`P256Verify.lean`)

Formal specification and proofs for the Ethereum EIP-7951 secp256r1 ECDSA signature verification precompile (`P256VERIFY`).

What was claimed: Formal specification and proofs for the Ethereum EIP-7951 secp256r1 ECDSA signature verification precompile (`P256VERIFY`).

What Lean states: 20 theorems in EthLib/Execution/Proofs/Evm/Precompiles/P256Verify.lean (ethereum/EthLib at 914134f6) — p256Verify_eq_error_iff, p256Verify_callData_eq_ok_valid_iff, p256Verify_callData_neg_s, and non-vacuity witness exists_p256Verify_eq_ok_valid.

Prose only / the gap: Elliptic-curve group law and p256Verify implementation live in imported EthLib.Cryptography.Proofs.Secp256r1.Ecdsa and EthLib.Execution.Evm.Precompiles.P256Verify.

Verification & replays: Static scan & 17 mutants generated by SeamCert (risk: low · 14). Kernel replay not run.

Open SeamCert static report & Mutants.lean →

What the public sources report

Every item below is attributed to the published paper, replay, or commentary that reported it.

Gas & length theorems p256Verify_eq_error_iff proves the call errors iff gas < GAS_P256VERIFY (6900). p256Verify_invalidInputLength proves any input size ≠ INPUT_BYTES (160) with sufficient gas returns .ok .empty. [1]
Signature malleability p256Verify_callData_neg_s proves that (r, s) and (r, Fn.modulus - s) yield identical precompile outputs at every gas limit, matching EIP-7951’s malleability specification. [1]
Explicit consistency witness Includes exists_p256Verify_eq_ok_valid : ∃ data : ByteArray, p256Verify data GAS_P256VERIFY = .ok VALID, ruling out vacuity on the happy path by signing hash 0 with key 1 and nonce 1. [1]
Escape hatches in file None (0 sorry, 0 axiom, 0 native_decide; uses kernel by decide on finite field constants). [1]

Open specification seams (our reading)

Our reading of the sources above: the places where the formal Lean statement and the informal headline claim can still come apart.

  • The custom callData packer in this file truncates each 32-byte big-endian word modulo 2^256; callers must pair p256Verify_callData_eq_ok_valid_iff with isValid_callData to see how raw 160-byte slices map to field elements.
  • The underlying secp256r1 parameters (Fp.modulus, Fn.modulus, Point.generator) and verify function are defined in imported EthLib modules, which belong in the audit scope.

Footnotes & Sources

  1. ethereum / EthLib — `EthLib/Execution/Proofs/Evm/Precompiles/P256Verify.lean` (commit 914134f6)

Sources read on 7 November 2026. Spotted an error or a newer independent replay? Write to [email protected].

Check your own statement file Order a Deep Audit →