--- ### Introduction to Formal Verification Formal verification transforms code into a mathematical format to ensure its correctness—think of it as an advanced form of unit testing. Historically, this technique was reserved for experts in the web three space, but with tools becoming more accessible, it's crucial for developers to master this skill. The stakes are high; a single error in a smart contract could result in the loss of vast sums of money. ### Demonstration of Three Formal Verification Tools #### Crafted Example Function To demonstrate the power of formal verification, I've crafted a function that's intentionally complex and error-prone to audit manually: - Operations are intentionally mismatched: additions are used for subtractions, divisions for additions, and so on. - Several similarly named variables (`number`, `nimbur`, `mumbu`, `nimbor`, `nimber`) are used, each with slight differences, adding to the complexity. - The function `hellFunc` is designed to never revert but contains numerous errors making it difficult to audit manually. #### Testing with Fuzzing First, we attempt to identify issues using fuzzing: - A test is set up to make a static call to `hellFunc`, asserting it does not revert. - Despite multiple test runs with increased iterations, fuzzing fails to detect any issues, demonstrating its limitations in this context. ### Formal Verification with Halmos, Control, and Certora #### Halmos - We take the same test used in fuzzing and apply Halmos for formal verification. - After running the test, Halmos successfully identifies a problem where the variable `number` set to 99 causes an issue, showcasing the effectiveness of converting the test into a mathematical problem and solving it. #### Control - The setup for Control is similar to that for Halmos, with the addition of the `KVM infinite gas cheat code` to handle complex computations. - The process is time-consuming, requiring potential breaks, but once completed, it allows for detailed inspection of where the test fails or passes. #### Certora - Certora requires the use of a special language designed for formal verification, CVL. - We establish a rule that `hellFunc` must never revert and set conditions to prevent storage randomization. - Running the Certora command provides a user-friendly interface to review the results, where it also pinpoints `number 99` as the problematic variable.
Formal Verification Speedrun
A comprehensive guide to formal verification in Solidity. The lesson shows how to use formal verification tools (Halmos, K, and Certora) to find bugs in your code and demonstrate the advantages that formal verification offers in comparison to traditional fuzz testing.
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
Guest lecturers:
Josselin Feist
Head of Blockchain at Trail of Bits
Last updated on January 17, 2025
Solidity Developer
Assembly and Formal Verification1. Introduction
A practical introduction to formal verification and symbolic execution - This lesson is focused on introducing the concept of formal verification and symbolic execution as applied to smart contracts. Using a code base for a math library, we walk through an initial audit and then explore the use of the Certora tool to test for bugs. Duration: 7min
2. Scoping
A beginner’s guide to performing a security audit on a Solidity smart contract codebase. This lesson covers the basic elements of a solidity audit, including an explanation of the different tools and techniques used to perform the audit. It demonstrates how to use Slither, Adern, and Foundry to identify bugs and security vulnerabilities. Duration: 7min
3. Wad Ray Rad
A brief overview of WAD, RAY and RAD in solidity. The lesson covers what these terms mean, and how they are used to define the number of decimal places for different tokens. Duration: 2min
4. Version Compatibility
A quick guide to checking for version compatibility in Solidity. The lesson covers checking for compiler compatibility using a library, which may be necessary when using inherited libraries. In this lesson, the compiler is incompatible with the library because the library requires a newer version of the compiler to support its features. Duration: 1min
5. Mulwad
A deep dive into the muWad function in Solidity - The lesson examines the code used in a muWad function within a Solidity contract. Specifically, it analyzes the assembly code in depth, breaking down each line and the various opcodes used, with the use of a helpful tool called Chisel. Duration: 12min
6. Reverting
A deep dive into memory and revert in Solidity - This lesson provides a deep dive into the memory and revert opcodes. It explores how the memory opcodes work in the context of the EVM, and how to use the revert opcode in Solidity to throw a custom error. Duration: 4min
7. Spotting The Bug
A detailed look at a Solidity memory demonstration - This lesson covers the differences between Solidity's mstore and revert opcodes and how they interact with memory. We also discuss how they work with the Free Memory Pointer. Duration: 7min
8. Incorrect Memory Access
A deep dive into Incorrect Memory Access Bug Recap - This lesson revisits the memory access bug and identifies the error in the code, then utilizes a memory diagram to demonstrate the correct way to handle memory allocation and reversion. Duration: 1min
9. Error Code Function Selector
A detailed explanation of the function selectors error code. The lesson covers examining the function signature and how it can lead to incorrect function selectors. The lesson also covers the function selector for revert in Solidity. Duration: 1min
10. Finishing Mulwad
A technical deep dive into the Solidity function `mulWadUp` and its assembly code - the video highlights an audit process for a Solidity function which reveals several instances of unusual assembly code being used, including a blank message revert and a `div` function, before going into a breakdown of how the assembly code for the `mulWadUp` function actually works. Duration: 1min
11. Mulwadup
A detailed explanation on Solidity's 'or' command - A closer look at Solidity's 'or' command. This lesson shows how the 'or' command works in Solidity, and walks through a quick debugging scenario. Duration: 1min
12. Where Fuzzing Fails
A comprehensive guide to finding a bug in Solidity code using fuzz testing. The lesson covers how to set up fuzz testing in Foundry and provides an example to show how fuzz testing can be used to find edge cases and errors that are difficult to find with traditional unit testing. Duration: 10min
13. Sqrt Function Intro
A comprehensive guide to auditing square root functions in Solidity - This lesson covers formal verification of the square root function and also highlights a potential edge case that might be missed by a fuzzer. The video will introduce the student to two different approaches to finding a square root: using the Babylonian method in assembly and using the Solmate library's approach. Duration: 6min
14. Formal Verification
A comprehensive guide to Formal Verification and Symbolic Execution - This video walks through a high-level overview of formal verification and symbolic execution, covering how they're used for security and testing in web3, and the path explosion problem. Duration: 15min
15. The 4 Stages Of Invariant Tests
A practical guide to formal verification for smart contracts - This lesson shows a repo that includes minimized examples of smart contract exploits as well as different testing techniques for them. It includes examples of stateless fuzzing, stateful fuzzing, stateful fuzzing with a handler, and formal verification. You'll also learn about the pros and cons of each. Duration: 10min
16. Where Fuzzing Fails 2
A deep dive into where fuzzing fails - This lesson looks at an example of a code base where a fuzzer would give the false impression that there are no bugs. It then goes on to explore some of the potential reasons why fuzzing might fail to find bugs, including the possibility that a fuzzer might not be run for long enough. The lesson also considers the idea that, while fuzzing might be a powerful tool, some codebases might be so complex that they require manual auditing instead of fuzzing. Duration: 3min
17. Formal Verification Speedrun
A comprehensive guide to formal verification in Solidity. The lesson shows how to use formal verification tools (Halmos, K, and Certora) to find bugs in your code and demonstrate the advantages that formal verification offers in comparison to traditional fuzz testing. Duration: 4min
18. Formal Verification Setup
A comprehensive guide to Formal Verification - This lesson covers how to write formal verification suites, using two tools: Halmos and Certora. The lesson also highlights the trade-offs between these two formal verification tools. Duration: 1min
19. Wsl Python Setup
A practical guide to creating a Python virtual environment. This lesson demonstrates how to install the virtualenv library, and create and activate a virtual environment to ensure that project dependencies are isolated and do not conflict with other projects on your system. Duration: 11min
20. Halmos Wsl
A quick guide to installing and running Halmos on your computer. This lesson covers installing and setting up Halmos, as well as writing a simple test using an ERC20 token and showing it in action. Duration: 2min
21. Halmos
A comprehensive guide to symbolic testing with Halmos. This lesson provides you with the basics of setting up your Halmos testing environment, writing a simple Halmos test, and using Halmos to help you prove or disprove your assertions. Duration: 12min
22. Certora
A practical guide to formal verification using Certora. This lesson covers the concept of formal verification, how Certora can be used to ensure the security of smart contracts, and how to use the Certora prover. Duration: 3min
23. Certora Wsl
A comprehensive guide to installing Certora on your WSL environment. This lesson will teach you how to set up a virtual environment, install the Certora package, and add your personal access key as an environment variable. Duration: 2min
24. Setting Up Our Spec And Conf Folders
A beginner’s guide to running Certora formal verification tools using a simple example. This lesson covers the basic setup for Certora formal verification, including creating a ‘specs’ and ‘conf’ folder, writing a rule and an invariant, and explaining the different parameters that you need to provide Certora. Duration: 8min
25. Installing Certora
A comprehensive guide to installing Certora and solc-select - This lesson covers how to install the Certora prover package and solc-select in a Linux-like environment to set up your Solidity development environment. The guide covers setting up your personal access key as an environment variable, and explains the different ways to install and switch between Solidity compiler versions with solc-select. Duration: 5min
26. First Certora Run
A simple guide to running the Certora prover - This video lesson covers how to run a Certora prover using a terminal command line. The lesson covers the details of how to write the command line and how to understand the output that is generated once the prover has completed. Duration: 4min
27. The Methods Block
A technical guide to writing methods in the Certora prover using the “methods” block. This lesson covers the basics of the “methods” block and explains how to specify different methods and their returns. It also discusses the concepts of “envfree” tags and how they affect the proving process. Duration: 2min
28. lastReverted
A simple guide to using invariants in Certora. The lesson covers the key elements of an invariant as it relates to Solidity smart contracts. It walks through how to use Certora to ensure a smart contract never reverts when being run. Duration: 1min
29. Analyzing A Failed Certora Run
A practical guide to analyzing a failed Certora run - In this lesson, you will learn how to analyze a failed Certora run, including how to understand the different parts of the call trace, how to identify the counter-example that caused the failure, and how to interpret the results of the run. Duration: 5min
30. Require Statements
A detailed explanation of require statements in Solidity for Formal Verification. This lesson discusses the need to specify pre-conditions for Certora to run correctly, and walks through using 'require' statements to declare the initial state of storage variables. Duration: 2min
31. Failed Certora Run 2
A comprehensive guide to identifying and debugging a failed Certora Run 2 - The lesson covers the process of identifying and resolving an issue with a formal verification check. This involves looking at the Certora output, tracing the call stack and then looking at the code in order to identify the bug. Duration: 3min
32. Envfree
A detailed guide to understanding the 'envfree' function, and how the environment can be used as a first parameter in function calls in Certora. This lesson covers what the 'envfree' keyword does, how to pass an environment into a function, and how to use the environment to find edge cases that can break your invariants or rules in Certora. Duration: 6min
33. Leveling Up Our Conf File
A practical guide to leveling up your configuration file - The video explores several key parameters within your Certora configuration file such as 'wait for results' and 'rule sanity'. You will learn how to use these parameters to optimize your formal verification process. Duration: 2min
34. Formal Verification Introduction Recap
A quick introduction to formal verification in Solidity. The lesson goes over how to use the Halmos and Certora tools to verify a simple rule or invariant for a solidity contract. This example will show how to write a rule that proves that a function will never revert. Duration: 2min
35. Using Formal Verification On Math Masters
A fun challenge in formal verification to Math Masters - This lesson will use Halmos and Certora to do formal verification of two Solidity functions: mulWadUp and sqrt. The lesson will also reveal the clue that should've tipped you off that there was an issue with the sqrt function and that it was not actually passing. Duration: 1min
36. Halmos Mulwadup
A practical guide to path explosions and timeouts in formal verification - This lesson covers the importance of using fuzzing first in formal verification, as well as how to increase Halmos’ run time by modifying its parameters. Duration: 7min
37. Certora Mulwadup
A comprehensive guide to verifying internal functions and libraries in Solidity - This lesson focuses on understanding the use of code harnesses to verify the functionality of internal functions and libraries, and introduces Certora, a formal verification tool. Duration: 6min
38. Formal Verification Soundness
A technical guide to formal verification soundness - This lesson discusses the concept of soundness in formal verification, particularly as it relates to the Certora prover. We see an example of an unsound approximation, and learn how to address this problem. Duration: 2min
39. Definitions
A detailed breakdown of definitions in the Certora Verification Language - This lesson explains how to use definitions to encapsulate commonly used expressions. You will learn how to declare a definition, how to use a definition, and what kind of expressions you can encapsulate within a definition. Duration: 1min
40. Refactoring
A detailed guide to refactoring for CVL - This lesson covers how to refactor code for the Certora Verification Language (CVL) including using the `require` keyword, the concept of `max_uint`, and the difference between `mathint` and `uint256` types. Duration: 5min
41. Your First Certora Invariant
A detailed guide to writing and understanding invariants in Certora - The lesson covers the definition of an invariant and how to write one using the invariant keyword, and explains the difference between an invariant and a rule. Duration: 6min
42. Invariant Preserved Blocks
A comprehensive guide to using invariants and preserved blocks in Certora. This lesson covers the process of rewriting a rule to be an invariant in Certora, as well as the differences between a rule and an invariant. The lesson also shows how to use preserved blocks in conjunction with invariants to establish conditions necessary for the invariant to hold. Duration: 3min
43. Certora Recap
A comprehensive recap of Certora invariants, harness, rules, and types - This lesson covers the basics of formally verifying internal functions using Certora. It explains how to use harness to wrap and verify the functionality of a function, and how to use definitions to define different types of variables. The lesson also demonstrates how to define rules, including pre-conditions and post-conditions, and how to use invariants to ensure the properties of the system hold. Finally, the lesson shows how to perform correct conversions between different types using the assert keyword. Duration: 2min
44. Tackling The Sqrt Function
A comprehensive guide to tackling the SQRT function - This lesson walks through the process of auditing a square root function by comparing different codebases and testing cases to find the most accurate and secure solution. We also learn how to utilize fuzz testing to identify any potential errors within the SQRT function. Duration: 2min
45. Naive Formal Verification With Halmos
A naive approach to formal verification with Halmos - The video goes over how to use Halmos and how naive formal verification can be. Halmos is a tool that is used to formally verify solidity code. Duration: 2min
46. Naive Optimistic Loop
A detailed guide to using the Certora prover for verifying the SQRT function. This lesson covers how to use Certora to verify that the SQRT functions in different libraries are equivalent to each other and will also walk you through how to debug timeout errors when using Certora. Duration: 8min
47. Modular Verification
A practical guide to modular verification for Solidity. The lesson discusses how to break a complex problem into simpler subproblems and how to verify each part separately. The video then walks through a real-world example of finding a bug in a square root function by utilizing modular verification and a fuzz test. Duration: 11min
48. Sqrt Function Hint
A practical guide to finding a bug in a square root function using modular verification - In this lesson, we explore the concept of modular verification and use it to locate a bug in a square root function. We will leverage the Certora tool to execute verification checks, ensuring that our code matches the intended behavior of the square root function. Duration: 3min
49. Modular Verification Recap
A comprehensive guide to formal verification in Web3 – Learn how to use Certora to test your Solidity code. The lesson covers modular verification, how to use Certora's different functionalities, and how to write a detailed formal verification audit report. Duration: 9min
50. Recap
A comprehensive guide to Formal Verification - Let's dive deep into the world of Formal Verification with a detailed overview of the process. We'll learn how to identify potential vulnerabilities and bugs in Solidity code and verify that the code is functioning as intended. Duration: 6min
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
Guest lecturers:
Josselin Feist
Head of Blockchain at Trail of Bits
Last updated on January 17, 2025
Testimonials
Students Reviews
Read what our students have to say about this course.
Chainlink
Chainlink
Gustavo Gonzalez
Solutions Engineer at OpenZeppelin
Francesco Andreoli
Lead Devrel at Metamask
Albert Hu
DeForm Founding Engineer
Radek
Senior Developer Advocate at Ceramic
Boidushya
WalletConnect
Idris
Developer Relations Engineer at Axelar