We've completed a security audit with @Optimism covering Supernode's Interop validation, spanning an initial 9-week review plus a 10-week extension, with final delivery in July 2026. The engagement combined design review, manual code review, formal verification using Dafny, and a fuzzing campaign, focusing on cross-chain message validation and database consistency under failure. Optimism's Supernode and Interop Filter extend the OP Stack's interoperability model, managing cross-safe and cross-unsafe verification of messages across L2 chains. Together, they let blocks be classified by safety level based on whether their cross-chain dependencies have been validated, not just their L1 availability. During the first phase, we produced a formal model of Supernode's core logic in Dafny, defined and proved key invariants (including cross-validity of verified entries and VerifiedDB/LogsDB consistency), and built a fuzzing harness exercising real production code (LogsDB, VerifiedDB, engine rewind path) against a Dafny-derived oracle. The extension strengthened previously partial invariants to full enforcement, explored an AI-assisted approach to systematically compare the Go implementation against the Dafny spec function-by-function, and expanded fuzzing to cover fault injection and adversarial rewind scenarios. The audit identified findings of varying severity across both components. Our teams worked side by side throughout the process, with several identified issues fixed during the review. We're proud to support Optimism in strengthening the security of the OP Stack, and grateful for their close collaboration!