← All programs
SCA-401Expert72h · 8 weeks (self-paced)
Advanced Smart Contract Audit & Formal Verification
The step from auditor to lead. Formal verification with Halmos and Certora, symbolic execution at scale, invariant synthesis, bridge and cross-chain methodology, MEV-aware review, and running an audit engagement end-to-end. Designed for reviewers who already have published findings and want to operate at the edge of the field.
01 · Outcomes
What you will be able to do.
- 01Prove non-trivial invariants with Halmos and Certora confidently
- 02Design symbolic-execution harnesses for real protocol code
- 03Lead bridge and cross-chain audits with layered threat models
- 04Hunt novel vulnerability classes under MEV-aware adversary models
- 05Run an audit engagement end-to-end with clients and team
02 · Syllabus
What you will cover.
Week 1-2
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
Week 3-4
Symbolic Execution & Invariant Synthesis
- →Path explosion, loop bounds, and modelling external calls
- →Differential and relational invariants across upgrades
- →Mutation testing as a completeness signal
Week 5
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
Week 6
MEV-Aware Review
- →Atomic composition attacks and sandwich vectors
- →Private-mempool assumptions and their failure modes
- →Oracle latency as an exploit primitive
Week 7
Novel Vulnerability Research
- →Reading protocol changelogs for new primitives
- →Building minimal PoCs from unfamiliar codebases
- →Documenting a finding that a stranger can reproduce
Week 8
Engagement Leadership
- →Scoping, timelines, and client expectation management
- →Running a review team with asymmetric skill levels
- →Post-audit remediation review and follow-through
Tools
- • Halmos
- • Certora Prover
- • Foundry
- • Medusa
- • ItyFuzz
- • Slither
Who it's for
- Working auditors ready to move from reviewer to lead
- Protocol security engineers building internal audit capability
- Researchers applying formal verification to real protocols
Prerequisites
- Completion of SCA-201 or 12+ months of active audit experience
- Comfort with Foundry invariant testing and basic symbolic execution
- At least one published finding or reviewed audit report
Ready?