Formal verification of Pectra system contracts with Halmos

1.30.25

Ethereum’s upcoming Pectra hardfork introduces several enhancements to user experience and validator operations across 11 EIPs. Three of these introduce onchain system contracts that use assembly language to optimize gas efficiency. While effective, the use of assembly raises security concerns due to its low-level nature and the lack of compiler-enforced safety checks.

One approach to navigating these risks is by using formal verification to eliminate potential assembly-level security vulnerabilities. To address this, we’ve used halmos, our formal verification tool, to ensure the correctness of Pectra system contracts, solidifying the security of the Pectra upgrade.

The resulting verification artifacts may also serve as concrete examples for other smart contracts that rely on assembly code. Although formal verification is often perceived as an abstract and complex concept, practical examples like these can showcase its utility in a wider range of situations.

In this post, we begin with a brief introduction to Pectra system contracts and the challenges of assembly implementation. We then break down formal verification processes into several steps, and show how we use halmos for these tasks.

Pectra systems contracts and the challenges of assembly implementations

As noted, the Pectra hardfork, scheduled to ship early this year, includes 11 EIPs, three of which introduce system contracts that execute onchain logic:

EIP-2935 proposes storing the last 8191 block hashes in a system contract to support stateless execution. This contract uses a ring buffer for efficient block hash storage.
EIP-7002 introduces a mechanism allowing validators to initiate exits and withdrawals directly via their execution layer withdrawal credentials, with withdrawal requests stored in a dedicated system contract. A queue is used here to manage withdrawal requests.
EIP-7251 proposes increasing the maximum effective balance for validators, allowing larger validators to consolidate operations. These consolidation requests are managed by a separate system contract using a queue.

Unlike typical smart contracts written in Solidity, these system contracts are written entirely in assembly for the sake of gas efficiency. Writing smart contracts in assembly language is not uncommon — Seaport and Solady are well-known examples — especially in scenarios where the Solidity compiler generates suboptimal code. Notable scenarios for suboptimal compilation include manipulation of byte arrays for calldata preparation, Keccak hash inputs, and other opcodes that read or write dynamic-sized bytes from/to memory.

While gas-efficient, assembly programming is a challenging practice, because it can easily introduce flaws and security vulnerabilities. When writing assembly, security checks handled by the compiler (e.g., calldata validation, memory sanitization, and implicit type casting) should be implemented manually.

Missing checks may result in invalid inputs or dirty memory being exploited, potentially leading to security vulnerabilities. Manually implementing these checks, however, requires advanced knowledge and is prone to human error. This overhead, combined with added complexities from low-level programming, make it extremely challenging and labor-intensive to produce secure assembly code.

Formal verification offers a systematic solution to address these challenges by providing mathematical guarantees of correctness and security.

A blueprint for formal verification

Let’s briefly introduce a basic framework for formal verification. While other frameworks exist and details may vary depending on target systems and contexts, this framework provides a useful mental model applicable to the Pectra system contracts. A full explanation of formal verification is beyond the scope of this post. For more information on formal verification of smart contracts, this guide is a good starting point.

A comprehensive approach to end-to-end formal verification typically involves the following steps, grouped into two phases:

Phase 1: Model verification

Step 1. Formalize specifications: Translate the specification, often presented in natural language (e.g., EIPs), into a formal specification language.
Step 2. Define properties: Identify the key properties that the specification must satisfy (e.g., ensuring the ring buffer in EIP-2935 always holds valid block hashes).
Step 3. Prove properties: Verify that the formal specification defined in Step 1 satisfies the properties identified in Step 2.

Phase 2: Refinement proofs

Step 4. Model implementation: Translate the implementation code into a mathematical model.
Step 5. Prove refinement: Show that the formal model of implementation (from Step 4) faithfully adheres to the formal specification (from Step 1).

Model verification and refinement proofs address different aspects of the verification process. Model verification ensures that the specifications are sound, while refinement proofs confirm that the low-level implementation aligns with the specifications. Together, these ensure that the implementation meets the key properties.

Separating concerns into these two phases provides clarity and modularity in the verification process. It also enables flexibility in execution, allowing different tools and methods to be applied to each phase, parallelizing tasks, or prioritizing them based on time and resource constraints.

In the context of Pectra contracts, model verification amounts to reasoning about their EIP specification document, while refinement proofs ensure that the implementation code matches the EIP document.

Choosing a tool

Developers can choose from a variety of tools, possibly different tools, for performing model verification and refinement proofs.

Model verification can benefit most from tools with versatility and expressiveness. Popular options include interactive theorem provers (e.g., Lean, Coq, Isabelle, ACL2), model checkers (e.g., TLA+, Alloy, Quint), and deductive verifiers (e.g., Dafny, Why3). These tools enable rigorous reasoning about the properties. For simpler specifications, manual pen-and-paper proofs could also be effective, though they increase the trust base and require meticulous review. Side note: integrating model verification with security audits can be highly beneficial, as auditors may identify additional security properties or potential vulnerabilities within the specification.

Refinement proofs can benefit from automated verification tools specific to their implementation language. Such automated tools (e.g., halmos, hevm, Kontrol, Certora for Ethereum smart contracts) can internally handle the modeling of implementation, reducing the risk of human error and the trust base associated with manual translation. Moreover, since implementation code often undergoes frequent changes due to optimizations or refactoring, automated verification can be particularly valuable for performing continuous verification. These tools streamline the process, ensuring that the implementation remains aligned with the specification without requiring exhaustive manual scrutiny for every code update.

With the formal verification framework in mind, we can now discuss how it can be applied to Pectra system contracts. Next, we will detail the use of halmos for refinement proofs. Note that our halmos-based formal verification specifically focuses on refinement proofs, excluding model verification. Model verification can be performed separately using the methods and tools discussed earlier, which we leave for future work.

Refinement proofs of Pectra system contracts

Halmos, a formal verification tool for EVM bytecode, is well-suited for performing refinement proofs. It automates key parts of the process, particularly Step 4 (modeling the implementation), and directly verifies refinement between the specification and the implementation bytecode in Step 5.

To use halmos, refinement conditions are expressed as regular Solidity tests, specifically using assertions to ensure the implementation’s behavior aligns with their specification. These assertions focus solely on verifying that the implementation adheres to the specification, distinct from validating the properties of the specification itself — a task handled during model verification.

We applied halmos to Pectra system contracts by manually translating the EIP specifications into Solidity test assertions. Then we used these tests to verify the compiled bytecode of the assembly implementation. This process ensures that the system contracts behave as specified, across all possible inputs and contract states. While Halmos provides a “bounded” formal guarantee — limited by execution constraints like loop iterations or byte array sizes — it is a robust and practical approach for ensuring correctness.

The trust base for this process includes the manual translation of EIP specifications to Solidity tests — reviewed independently by our security engineer — and the halmos tool itself. Importantly, the assembly compiler is excluded from the trust base, as the verification directly targets the compiled bytecode.

Efficiency and continuous verification

We completed the initial verification process within a few days and later improved over a couple of weeks to enhance test structure, assertions, and documentation. Halmos proved effective for both the initial verification and the continuous verification process, which involved re-verifying the implementation after code updates. Each re-verification cycle required only a few hours, making it practical to maintain correctness even during iterative development.

The value of continuous verification was underscored when halmos tests detected an off-by-one error introduced during a refactoring process. Refactoring, by definition, should preserve the original behavior of the code. However, the tests failed, signaling a discrepancy. A deeper investigation uncovered a subtle mistake, highlighting continuous verification as a powerful safety net for catching errors early in iterative changes and reinforcing code reliability.

For full details and access to the artifacts from our formal verification of Pectra system contracts, see here.

***
We see formal verification as a useful approach for a wide audience of developers and security researchers — not just a select set of experts. If you’re working on gas-optimized contracts or curious about formal verification, now’s the time to dive in. As assembly optimization remains a critical practice for achieving gas efficiency, integrating formal verification tools like halmos into the development process provides a practical way to balance performance with security. This approach not only enhances confidence in low-level implementations but also demonstrates that optimization and security can coexist without compromise.

***
We thank @lightclients, Felix Lange, Fredrik Svantes, and Ignacio Hagopian for sharing their insights on the design decisions of system contracts; Matt Gleason, Taek Lee, and Jinwoo Lee for their valuable discussions and contributions during the verification process; Eddy Lazzarin, Sophia Gold, and Tim Beiko for facilitating collaboration; and Stephanie Zinn and karma for their thoughtful feedback and review of this post.

***

The views expressed here are those of the individual AH Capital Management, L.L.C. (“a16z”) personnel quoted and are not the views of a16z or its affiliates. Certain information contained in here has been obtained from third-party sources, including from portfolio companies of funds managed by a16z. While taken from sources believed to be reliable, a16z has not independently verified such information and makes no representations about the current or enduring accuracy of the information or its appropriateness for a given situation. In addition, this content may include third-party advertisements; a16z has not reviewed such advertisements and does not endorse any advertising content contained therein.

This content is provided for informational purposes only, and should not be relied upon as security, legal, business, investment, or tax advice, nor as an endorsement of any such practices, products or services. There can be no guarantees or assurances that the views expressed here will be applicable for any particular facts or circumstances, and they should accordingly not be relied upon in any manner. References to any securities or digital assets are for illustrative purposes only, and do not constitute an investment recommendation or offer to provide investment advisory services. Furthermore, this content is not directed at nor intended for use by any investors or prospective investors, and may not under any circumstances be relied upon when making a decision to invest in any fund managed by a16z. (An offering to invest in an a16z fund will be made only by the private placement memorandum, subscription agreement, and other relevant documentation of any such fund and should be read in their entirety.) Any investments or portfolio companies mentioned, referred to, or described are not representative of all investments in vehicles managed by a16z, and there can be no assurance that the investments will be profitable or that other investments made in the future will have similar characteristics or results. A list of investments made by funds managed by Andreessen Horowitz (excluding investments for which the issuer has not provided permission for a16z to disclose publicly as well as unannounced investments in publicly traded digital assets) is available at https://a16z.com/investments/.

Charts and graphs provided within are for informational purposes solely and should not be relied upon when making any investment decision. Past performance is not indicative of future results. The content speaks only as of the date indicated. Any projections, estimates, forecasts, targets, prospects, and/or opinions expressed in these materials are subject to change without notice and may differ or be contrary to opinions expressed by others. Please see https://a16z.com/disclosures for additional important information.