Ethereum Foundation grants $100K for Vyper compiler formal verification

The Ethereum Foundation has awarded a $100,000 grant to a formal-verification effort targeting the Vyper compiler, part of a $600,000 allocation announced under the ETHSecurity Initiatives Round Two program, according to Crypto Briefing. The work is led by the Foundation for Verified Software together with Verifereum, the group publishing a formal model of Ethereum in the HOL4 proof assistant. It builds on the initial EF Ecosystem Support Program grant FY25-1892.

What the grant funds

The stated goal is a "verified compilation" mode built directly into the official Vyper compiler, backed by a mathematical proof that the compiler's translation from Vyper source to EVM bytecode preserves the program's meaning. The work sits at the layer contract audits do not cover: even a formally verified Vyper contract can be miscompiled by a buggy compiler, and the bytecode that lands on-chain is what matters.

Concretely, the effort:

• Publishes a formal semantics for Vyper in HOL4 (the Verifereum repo's vyper-hol is the working artifact).
• Extends Verifereum's existing HOL4 model of the EVM.
• Wires the two together so that, for a given Vyper source, a proof mechanically checks that the emitted EVM bytecode implements the specified semantics.
• Ships the result as a compiler mode developers and auditors can opt into.

The prior work being extended is documented in the Verifereum project's GitHub repo and the broader ecosystem overview maintained by Leonardo Alt.

Why this exists

The reference incident is 2023's Curve reentrancy exploit. The bug was not in application code: the affected Curve pools used a Vyper-implemented reentrancy guard that was correct at the source level. A miscompilation in Vyper versions 0.2.15, 0.2.16 and 0.3.0 silently disabled the guard in the emitted bytecode. Attackers drained roughly $70 million across several pools — including CRV/ETH, alETH/ETH, msETH/ETH and pETH/ETH — before mitigation.

That failure mode is what verified compilation is designed to eliminate. Every audit that reads Vyper source implicitly trusts the compiler; a verified compilation mode moves that trust into a machine-checkable proof. The security-model consequence is significant: the source of an audited contract becomes the object being verified, rather than an artifact to argue about against unverified toolchain output.

Numbers block

• Grant size: $100,000 (this award)
• Program total: $600,000 across ETHSecurity Round Two
• Recipients: Foundation for Verified Software, Verifereum contributors, Vyper dev team
• Prior grant reference: FY25-1892 (Ethereum Foundation Ecosystem Support)
• Proof assistant: HOL4 (higher-order logic)
• Repo: github.com/verifereum/vyper-hol
• Motivating exploit: 2023 Curve reentrancy (~$70M across pools, Vyper 0.2.15/0.2.16/0.3.0)
• Sources: Crypto Briefing, Verifereum GitHub, ethereum.org / Verifereum

What to watch

1. Merge timelines into the mainline Vyper compiler. The verified mode is only useful if it lands in the official compiler that projects already build against. Watch the Vyper GitHub for tracking issues and design PRs from Foundation for Verified Software contributors.
2. Coverage of the Vyper feature surface. HOL4 semantics for a subset is easier than semantics for the full language. The initial deliverable will disclose which language features (calls, delegatecalls, immutables, decorators) are inside the verified core.
3. Comparable work on Solidity. The Solidity project has parallel initiatives — SMTChecker, Certora, Runtime Verification's K semantics. A Vyper-first verified compilation mode adds pressure on Solidity to reach parity.

Context

This is the second concrete step from the Ethereum Foundation's ETHSecurity Initiatives program launched earlier in 2026, after the initial funding round that put money into audit-tooling and MPC-fuzzing research. The Foundation has been explicit that $100K is a seed amount and additional ecosystem contributions are expected. The move fits a broader pattern across L1s of treating compiler and toolchain correctness — not just contract logic — as a first-class security surface, after a decade of exploits where compilers were the silent load-bearing dependency.