Introduction¶
This tutorial builds upon concepts covered in the main Certora Prover Tutorials such as propositional & predicate logic, and the basics of formal verification. If these are not already familiar to you, refer to section 1 of the Certora Prover Tutorials before proceeding.
What is Certora Sunbeam?¶
Sunbeam is a tool for formally verifying Soroban smart contracts written in Rust. You can leverage Certora’s Cavelier (CVLR) library to write specifications for such contracts in Rust also. You can read more about Sunbeam in the User Guide for Sunbeam documentation.
The project¶
The tutorial project’s directory is in projects/token. Below is a brief description of this Rust project directory’s contents:
src/lib.rs has a Soroban smart contract with some functionality of a Token.
confs/ has several configuration files to help you run Certora Sunbeam.
src/certora/ is where we will write the formal specs for this contract. It also has a directory of
mutantsto evaluate the specs.
Solutions¶
In file solutions/solution_specs.rs you’ll find the solutions to all exercises of this repository. You can consult it if you want to know the answers.