In 2024, we released a paper on the security of Blockchain Rollups in collaboration with Matter Labs. The paper analyzes the security of blockchain rollups and introduces a formal model to reason about different mechanisms. You can find the paper on arxiv. In this blog post, we will discuss the security of Rollups and provide a gentle introduction to what we did in our paper.

In his recent blog post, Vitalik Buterin highlighted that while Ethereum aims to be a robust, multi-purpose blockchain, there is only so much it can handle on its own. To maintain decentralization and security, Ethereum itself must resist shortcuts—leading to a cap on how much capacity (“scalability”) we can squeeze out of the base layer.

Enter the Rollups

Rollups mitigate this problem by moving transactions off the main chain to a Layer 2 (L2) chain, thus significantly increasing throughput while still inheriting Ethereum’s security (more on that later). Two prevalent types of rollups have emerged:

• Optimistic Rollups: Assume that “batched” transactions are correct and rely on on-chain challenges or fraud proofs if something is suspected to be wrong.
• ZK-Rollups: Rely on cryptographic proofs (Zero-Knowledge Proofs – or more precisely, succinct proofs) so that invalid batches simply cannot be finalized on Ethereum.

Vitalik’s blog post emphasizes that rollups aren’t just a short-term fix. They’re now a central element of Ethereum’s long-term vision, tying together the broader roadmap that includes increasing data availability. By bundling transactions “off-chain” and confirming them “on-chain,” rollups balance scalability and security in a way that pure on-chain scaling alone cannot accomplish without compromising other aspects.

In practice, rollups are new chains that post and validate their state updates (or transactions) on the L1 blockchain.

L2BEAT and the Race for Safer and Cheaper Transactions

The L2BEAT team has made a significant effort to bring awareness to the growth and maturity of L2 solutions (especially rollups). Beyond growth metrics, L2BEAT introduced a “stages” framework that aims to clarify how mature each L2 is. These “stages” do not measure code complexity; they reflect governance structures, decentralization of sequencers, and how quickly a user can exit if something goes wrong.

Summarizing the main points of L2BEAT’s stages:

• Stage 0: Early projects with a centralized or “training wheels” model.
• Stage 1 & 2: Steps toward more decentralized control over upgrades and proofs. Some trust in operators remains.
• Stage 3 & Beyond: Final or near-final maturity, featuring robust censorship resistance, minimal trust in operators, and well-defined upgrade paths with timelocks or community governance.

L2BEAT’s perspective helps the community understand that “decentralized enough” is not a single moment. Instead, it’s a roadmap of incremental changes that eventually deliver the same trust properties as Ethereum.

Beyond Maturity Labels

So far, we have taken it for granted that L2s inherit or benefit from Ethereum’s security. Security on L1 means that an attacker would need to corrupt a large portion of the network’s nodes to make even a single transaction fail. To say that an L2 inherits the security and censorship resistance of L1, a few properties must hold. To the best of our knowledge, no general-purpose rollup truly inherits the security of L1 at the moment. Note that L2 blockchains are typically quite centralized to achieve higher throughput and cost efficiency (in most cases, just a single centralized operator).

Intuitively, L2 users must be able to verify that their transactions have been included and correctly executed on the L1 (data availability on L1 plus either cryptographic proofs or fraud proofs and a challenge period). Beyond that, users must be able to submit transactions through the L1 in case the L2 censors them. Finally, upgrades on the L2 should be announced on the L1 and have a timelock until they are applied, so users can exit if the upgrade is harmful to them.

Currently, in most L2s, if an attacker manages to gain control of the multisig that controls the L2 smart contract on L1, they can potentially “rug” the L2 and seize all user funds by applying a malicious upgrade. For example, in a ZK-Rollup, they could update the verifier to accept any proof. As some L2s might also want a “benign” blacklisting mechanism (e.g., for regulatory reasons), they may need complex additional features to meet all these requirements.

A Formal Foundation for Rollup Security

While maturity frameworks (like L2BEAT’s stages) give a high-level overview of how decentralized and user-friendly a rollup is, they don’t always dig into precise, formal guarantees. Our paper, “Towards a Formal Foundation for Blockchain Rollups,” aims to do exactly that:

1. Propose a rigorous specification of the key security properties a rollup protocol must fulfill.
2. Use formal methods (specifically model checking through Alloy) to verify whether a rollup’s design upholds these properties.

In particular, our work drills down into three crucial mechanisms that define a truly trust-minimized rollup:

1. Forced Transactions (Forced Queue)

   • What It Is: A way for users to bypass sequencer censorship by pushing a transaction straight to Ethereum’s L1 contracts.
   • Why It Matters: Even if the rollup sequencer is down or malicious, user transactions cannot be blocked.

2. Safe Blacklisting

   • What It Is: If a rollup chooses to incorporate blacklisting (e.g., for regulatory reasons), it must be done in a way that does not trap legitimate user transactions or break the forced queue.
   • Why It Matters: Balances the real-world need for blacklisting certain addresses with the fundamental principle of user control over their funds.

3. Upgradeability

   • What It Is: Rollup contracts often need to evolve, whether to add features or fix bugs, but a naive upgrade can be exploited or used to “rug pull” user funds.
   • Why It Matters: By imposing an on-chain enforced waiting period and guaranteeing that all forced transactions are processed before an upgrade, users have enough time to exit if they disagree with the changes.

How Formal Analysis Helps

Using Alloy – one of the best-known high-level modeling tools – we can systematically explore every possible combination of rollup-state transitions up to a certain scope. This approach spotlights corner cases in the design phase, effectively letting us say: “If there’s a situation where a forced transaction is censored anyway, Alloy will find it.”

This is complementary to L2BEAT’s stages, which define a progressive path to reduce trust. In other words, while L2BEAT tells you where a rollup sits on the decentralization journey, formal analysis helps ensure a rollup’s core contract logic is watertight – and that it truly enforces the minimal trust assumptions it claims to provide.

Why This Matters for Ethereum’s Future

• Protecting Billions in Assets: Rollups increasingly secure significant funds. Formal methods can help guarantee that no corner-case “rug pull” or permanent transaction censorship is possible.
• Building Ecosystem Credibility: As Vitalik’s blog post underscores, rollups are a core part of Ethereum’s roadmap. Rigorously specifying and verifying them fosters trust among users and ecosystem developers.
• Aligning with Maturity Models: Our formal approach can refine the L2BEAT stages, making them even more informative. If a rollup claims to be Stage 3, formal verification can demonstrate whether its forced transaction queue or upgrade path truly meets that standard.

Conclusion

Ethereum is moving deeper into a rollup-centric future, as highlighted in Vitalik’s blog post. L2BEAT’s maturity stages help us appreciate how different L2s are progressing on the decentralization journey. But to make sure these rollups really do what they claim – especially under worst-case scenarios – we need formal, mathematical verification of their key mechanisms. That’s exactly what our paper sets out to do.

If you want to learn more about our framework or if you’re working on an L2 and would like to apply our Alloy model to your mechanism, feel free to reach out.