Towards Universal Atomic Composability: A Formal Model for Multi-Rollup Environments on Ethereum

This paper introduces a formal framework for analyzing atomic composability in multi-rollup environments on Ethereum. As the blockchain ecosystem evolves towards a multi-rollup future, ensuring atomic execution of cross-rollup transactions becomes increasingly critical. We present a mathematical model that formally defines atomic composability in this context and establish necessary conditions for achieving it across different rollup systems.

Our work makes several key contributions:

• A formal definition of universal atomic composability for multi-rollup environments
• A mathematical framework for analyzing cross-rollup transaction properties
• Proof of necessary and sufficient conditions for atomic execution
• Analysis of existing cross-rollup protocols against our formal model

The findings have important implications for the design of cross-rollup bridges and protocols, suggesting new approaches for achieving robust composability in the growing rollup ecosystem.

Why composability breaks when execution moves off a single chain

On a single Ethereum execution environment, “atomic composability” is close to free: a transaction that calls into several smart contracts either completes all of its state changes or none of them, because the whole call graph executes within one virtual machine’s single state transition. The moment execution is split across multiple rollups — each with its own sequencer, its own state, and its own finality timeline — that guarantee no longer comes for free. A transaction that needs to touch state on rollup A and rollup B has no single virtual machine boundary enforcing “both or neither”; each rollup can only directly guarantee atomicity over its own local state.

What a formal model buys you that intuition doesn’t

Cross-rollup bridge designs are usually justified informally — “this should be safe because X” — which is exactly the kind of reasoning that has produced expensive bridge exploits when an edge case wasn’t considered. A formal model forces the necessary conditions for atomic execution to be stated precisely enough that they can be checked against a specific protocol design, rather than argued about qualitatively. That’s the difference between “we believe this bridge preserves atomicity” and “this bridge satisfies conditions 1 through N, which we have proven are necessary and sufficient” — the latter can actually be falsified by checking a design against the conditions, which is what makes the formal approach useful for evaluating protocols that already exist, not just designing new ones.

Why this matters beyond any one bridge design

The multi-rollup ecosystem is still adding new rollups and new bridging approaches, and each one faces the same underlying composability problem regardless of its specific technical choices. A general formal model — rather than a proof specific to one bridge — is valuable precisely because it gives protocol designers a shared standard to check new designs against, instead of every new bridge having to reconstruct an informal safety argument from scratch and hope it holds up under adversarial conditions it didn’t anticipate.

What “necessary and sufficient” buys over “sufficient” alone

Many safety arguments in distributed systems only establish sufficient conditions — “if you do X, Y, and Z, the system is safe” — without establishing whether some subset of those conditions was actually load-bearing. Establishing necessary conditions alongside sufficient ones tells a protocol designer which requirements cannot be relaxed without losing the atomicity guarantee entirely, which matters directly for anyone trying to optimize a cross-rollup protocol for lower latency or cost: it draws the line between trade-offs that are safe to make and ones that quietly reintroduce the composability failure the model was built to prevent.