Optimism Deposit Transaction
Ethereum L2 Rollup
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.
Optimism Labs engaged Runtime Verification for a pilot formal verification project focused on the correctness of critical rollup infrastructure. The engagement targeted the depositTransaction function in the OptimismPortal contract—an essential mechanism for ensuring censorship resistance by allowing users to submit transactions directly from Ethereum L1. Using KEVM-Foundry, a beta integration of KEVM with the Foundry testing framework, Runtime Verification aimed to prove that all valid Foundry fuzz tests for this function hold universally, ensuring that the correct event is always emitted except in clearly invalid scenarios. The project involved both strengthening the formal assumptions and theorems specific to the Optimism codebase and advancing the KEVM-Foundry tooling itself. This work represents a key step toward applying full mechanized formal verification to real-world rollup systems.
Reports
Download the audit artifacts
Access the published PDF deliverables associated with this engagement.
PDF report 1
Optimism-Formal-Verification-Report.pdf
Download the published report for this engagement.