Formal Verification Game Plan

In this lesson we outline our roadmap to approach this NFT repo and how we'll use various formal verification techniques to verify and secure it.

Smart Contract Security Auditor Assembly and Formal Verification
1. Introduction
Introducing the final section of the Assembly EVM Opcodes and Formal Verification Course! Strap in for one more! Duration: 6min
2. Setup
We walk through setting up the Gas Bad NFT Marketplace locally and begin discussing the code base. Duration: 2min
3. Emitting Logs With Assembly Log 4
Patrick demonstrates efficient gas usage for logs through assembly code, explaining key parts and stressing the need for accurate event emission checks during audits. Duration: 3min
4. Formal Verification Game Plan
In this lesson we outline our roadmap to approach this NFT repo and how we'll use various formal verification techniques to verify and secure it. Duration: 3min
5. Verifying NFTmock
Patrick uses Certora's prover to formally verify our NFTMock contract! Duration: 4min
6. totalSupply > 0
In this video, Patrick demonstrates the process of creating invariants or rules for smart contracts using Certora, ensuring that the total supply of NFT tokens is never negative. Duration: 7min
7. Proving Minting Nfts
In this lesson we set up and run tests to verify that minting does in fact only mint one NFT. Duration: 5min
8. Parametric Rules
In this lesson, Patrick explains Parametric rules and how they're used with respect to Certora's prover. Duration: 5min
9. NFTmock Verification Recap
Lesson covers syntax & functionality of rule checks, emphasizing invariants as a vital tool for verification. Patrick touches on the importance of sanity checks. Duration: 2min
10. Formal Vertification Setup
Patrick focuses on setting up and optimizing verification process with detailed guidance on config files, contract code, and prover args. Duration: 2min
11. Ghosts and Hooks
Patrick teaches how to use ghost variables and hooks to enforce proper event emissions in Solidity smart contracts and Certora. Duration: 8min
12. init_state and Axioms
Key focus on initializing ghost variables and creating an initial state axiom, writing rules and invariants for storage updates and event omissions to ensure their validity. Duration: 5min
13. Analyzing Certora Errors 3
Patrick dives deep into a call trace to determine the cause of errors found by Certora's prover. Duration: 9min
14. Persistent Ghosts
Patrick outlines the use of the `persistent` keyword in Certora and it's application to ghost variables in formal verification tests. Duration: 1min
15. Method Summaries Introduction
Patrick introduces us to method summaries and method blocks in this lesson about additional Certora features. Duration: 3min
16. Method Entries Introduction
Patrick covers various ways to define functions for contracts in Certora, including exact entries, wildcard entries, summary declarations, catch-all entries, visibility modifiers, and function options. He emphasizes the flexibility and control available when specifying how functions interact with a system. Duration: 2min
17. Summary Declaration Examples
Patrick explains different types of function summaries like view, Havoc, and dispatcher, their usage and benefits. Duration: 2min
18. Summary Implementations
Patrick details explicit assumptions, Certora's dispatcher and their importance. Duration: 14min
19. Optimistic Fallback Prover Args
This lesson emphasizes using Prover Args for argument configuration and setting OptimisticFallback to true. Patrick explains the importance of exploring different Prover Arg types for tailored configurations. Duration: 2min
20. Vacuity
This video focuses on vacuity issues in rule problems, demonstrating how unchecked assertions can arise when no input satisfies all requirements defined by the spec. Duration: 3min
21. Mid Lesson Recap
We recap topics covered so far and the advantages of leveraging formal verification. Duration: 2min
22. Equivalence Checking Solidity Reference
In this video, Patrick demonstrates a rule in Cetora for formal verification proofs. The rule involves an undefined method variable and ensures that calling a function results in 2 contracts having the same state. Duration: 3min
23. Method Filtering
Patrick explains how to filter rules in a code base using Satora prover for more efficient verification Duration: 2min
24. Using
In this lesson, Patrick details the functionality and use of the `using` keyword. Duration: 1min
25. Finishing The Rule
Patrick suggests methods to address issues flagged by Certora and ensure successful comparisons between contracts. Duration: 10min
26. Do You Understand How Cool Is This
We take a moment to appreciate the power and potential of tools like formal verification in securing web3. Duration: 2min
27. Recap
Patrick discusses various concepts learned during the course, including prover arguments, summary types, ghost variables, Certora hooks, and formal verification. He highlights the importance of learning and career growth, and encourages CodeHawks contest participation. Duration: 8min

Course Overview

About the course

What you'll learn

Assembly

Writing smart contracts using Huff and Yul

Ethereum Virtual Machine OPCodes

Formal verification testing

Smart contract invariant testing

Halmos, Certora, Kontrol

Course Description

Who is this course for?

  • Smart contract security researchers
  • Advanced Smart contract engineers
  • Chief Security Officiers
  • Security professionals

Potential Careers

Security researcher

$49,999 - $120,000 (avg. salary)

Smart Contract Auditor

$100,000 - $200,000 (avg. salary)

Meet your instructors

Patrick Collins

Patrick Collins

Founder at Cyfrin

Web3 engineer, educator, and Cyfrin co-founder. Patrick's smart contract development and security courses have helped hundreds of thousands of engineers kickstarting their careers into web3.

Guest lecturers:

Josselin Feist

Josselin Feist

Head of Blockchain at Trail of Bits

Last updated on June 6, 2025