Course content.
8 weeks (self-paced) · 72 hours · 6 lessons
Formal Verification Foundations
Hoare logic, pre/post-conditions, and invariants in practice · Halmos end-to-end: proving ERC-4626 and vault invariants · Certora Verification Language and rule design
Symbolic Execution & Invariant Synthesis
Path explosion, loop bounds, and modelling external calls · Differential and relational invariants across upgrades · Mutation testing as a completeness signal
Cross-Chain & Bridge Security
Lock-and-mint vs burn-and-mint threat models · Message-passing layer attack surface (LayerZero, CCIP, Wormhole) · Replay, finality, and reorg assumptions across L1s and L2s
MEV-Aware Review
Atomic composition attacks and sandwich vectors · Private-mempool assumptions and their failure modes · Oracle latency as an exploit primitive
Novel Vulnerability Research
Reading protocol changelogs for new primitives · Building minimal PoCs from unfamiliar codebases · Documenting a finding that a stranger can reproduce
Engagement Leadership
Scoping, timelines, and client expectation management · Running a review team with asymmetric skill levels · Post-audit remediation review and follow-through