Video: Gas Bad NFT Marketplace - Optimistic Fallback Prover Args

Support

_Follow along with this video:_ --- ### Optimistic Fallback Prover Args In the last lesson we saw our verification HAVOCing because Certora didn't know how to resolve the low level `call` function executed within withdrawProceeds. So, how do we account for these arbitrary calls with the prover? Introducing: [**Prover Arguments**](https://docs.certora.com/en/latest/docs/prover/cli/options.html#prover-args) Prover arguments (prover_args) are CLI (or conf file) options which can be used to fine tune the behaviour of the prover. I greatly encourage you to read through the options available on the Certora Docs. For our purposes, we want to consider the `-optimisticFallback` option is going to be useful. ::image{src='/formal-verification-3/19-optimistic-fallback-prover-args/optimistic-fallback-prover-args1.png' style='width: 100%; height: auto;'} Let's apply this argument to our `GasBad.conf`. ```js { "files": [ "src/GasBadNftMarketplace.sol:GasBadNftMarketplace", "src/NftMarketplace.sol:NftMarketplace", "test/mocks/NftMock.sol:NftMock" ], "verify": "GasBadNftMarketplace:certora/spec/GasBadNft.spec", "wait_for_results": "all", "rule_sanity": "basic", "optimistic_loop": true, "msg": "Verification of NftMarketplace", "prover_args":[ "-optimistic_fallback true" ] } ``` Any of the options we add to this `prover_args` list will act as though we passed that option to our CLI command when running the prover! > ❗ **NOTE** > As of May 25, 2024 the above conf configuration may not work. You can pass this option _with_ your CLI command if necessary: `certoraRun ./certora/conf/GasBadNft.conf --optimistic_fallback` ### Wrap Up Ok, we have `prover_args` configured and we've constructed our method block to include `wildcard entries` as well as summary declarations. With all of this defined, let's run the prover again. ```bash certoraRun ./certora/conf/GasBadNft.conf ``` See you in the next lesson for the results!

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.

Prover Args

Last updated on March 15, 2024

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

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

Head of Blockchain at Trail of Bits

Last updated on June 6, 2025

Thanks for checking us out

Start learning for free

Start for free

Smart Contract Security Auditor Assembly and Formal Verification

Section 1: Introduction

Duration: 30min

Section 2: Horse Store

Duration: 4h 38min

Section 3: Math Masters

Duration: 3h 57min

Section 4: Gas Bad NFT Marketplace

Duration: 1h 56min

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

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