Optimism Pausability
Ethereum Layer-2
Critical / High
Medium
Low / Informative
Report files
Audit lifecycle
This engagement is complete with finalized deliverables.
Completed
Scheduled
Scope, timeline, and review plan were agreed.
Completed
In Progress
Manual review and verification work were carried out.
Completed
Completed
The engagement wrapped with a published final report.
Executive Summary
High-level assessment and conclusions
A concise overview of the audit scope, core findings, and the key outcomes from the engagement.
The goal of this engagement was twofold: first, verify Optimism's pausability mechanism for the L1 contracts, and second, ensure that the mechanism is verified as Optimism's code evolves. about? Optimism L1 contracts have a security mechanism that allows L2-to-L1 transactions to be paused. This means that, if necessary, governance can prevent L2-to-L1 transactions from being finalized by the pertinent L1 contracts.
To ensure that the verification considered the whole system as it is intended to be deployed rather than an isolated contract, we developed a new feature in Kontrol that leverages Foundry's recent state diff recording capabilities to faithfully include the relevant parts of the deployment sequence as the initial configuration to perform the verification. A follow-up post will describe in detail the mechanism.
Read more about this engagement on our blog: https://runtimeverification.com/blog/kontrol-integrated-verification-of-the-optimism-pausability-mechanism
Reports
Download the audit artifacts
Access the published PDF deliverables associated with this engagement.
PDF report 1
Optimism Proofs.md
Download the published report for this engagement.