Welcome to the documentation page

This was built using Lean 4 at commit 69a1d0485e241a494d69d3e2c98ad988f4396dcd

Clickable documentation of Fraud-Proofs Games implemented at A Secure Sequencer and Data Availability Committee for Rollups.

Protocols implemented:

Local L2

L2 blocks validity is defined local to the block. E.g.: all elements are valid, there are no duplicates within the block and block hashes matches Merkle root hash.

History L2

L2 blocks validity is defined based on the history of the protocol. In particular, there are no duplicates across history.