# Towards a Formal Foundation for Blockchain Rollups

arXiv: https://arxiv.org/abs/2406.16219 · HTML: https://mlsanity.com/paper/2406.16219/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Jun 2024.

## Built on by (most cited first, 1 of 1)

- [Agent Harness Distillation: Inference-Time Harness Extraction and Exploitation in Autonomous Multi-Agent Systems](https://mlsanity.com/paper/2607.28147/) (2026)

## Abstract (arXiv)

Blockchains like Bitcoin and Ethereum have revolutionized digital transactions, yet scalability issues persist. Layer 2 solutions, such as validity proof Rollups (ZK-Rollups), aim to address these challenges by processing transactions off-chain and validating them on the main chain. However, concerns remain about security and censorship resistance, particularly regarding centralized control in Layer 2 and inadequate mechanisms for enforcing these properties through Layer 1 smart contracts. In their current form, L2s are susceptible to multisig attacks that can lead to total user funds loss. This work presents a formal analysis using the Alloy specification language to examine and design key Layer 2 functionalities, including forced transaction queues, safe blacklisting, and upgradeability. Through this analysis, we identify pitfalls in existing designs and introduce an enhanced model that has been model-checked to be correct. Finally, we propose a complete end-to-end methodology to analyze rollups' security and censorship resistance based on manually translating Alloy properties to property-based testing invariants, setting new standards.