Using the Solana Certora Prover

Overview

This document provides a guide on how to use the Solana Certora Prover. It details configuration formats, the build process, and how to execute verification locally and remotely.

Project Structure

A typical Solana project integrated with the Solana Certora Prover includes:

• A Solana smart contract written in Rust.

• Configurations for running the Certora Prover: the Prover can be executed either by starting from source files or by verifying pre-compiled code.

The Certora Solana Examples repository contains a collection of example projects.

Configuration Formats

Running from Sources

This configuration mode calls cargo certora-sbf for building the project.

{
    "msg": "Message describing the rule",
    "rule": "rule_solvency",
    "optimistic_loop": false,
    "loop_iter": 3
}

Information relevant for Certora is fetched from the Cargo.toml file in the package.metadata.certora section:

# Rest of the Cargo.toml file to build the project.
# ...

[package.metadata.certora]
sources = [
    "Cargo.toml",
    "src/**/*.rs"
]
solana_inlining = ["certora/summaries/cvlr_inlining_core.txt"]
solana_summaries = ["certora/summaries/cvlr_summaries_core.txt"]

Verifying Pre-Built Contracts

This configuration mode explicitly specifies the pre-built files required for verification:

{
    "files": [
        "solana_contract.so"
    ],
    "solana_inlining": "../../cvt_inlining.txt",
    "solana_summaries": "../../cvt_summaries.txt",
    "process": "sbf",
    "optimistic_loop": false,
    "rule": "rule_solvency"
}

Key Differences:

• Verifying Pre-Built Contracts: Uses pre-compiled .so files for verification.

• Running from Sources: Builds the project by calling cargo certora-sbf. Furthermore, fetches the metadata for the Prover from the Cargo.toml file.

Execution Examples

Running from Sources

To run the Certora Prover using the “running from sources” configuration:

certoraSolanaProver sources_config.conf

Expected Output:

INFO: Building by calling ['cargo', 'certora-sbf', '--json']
Connecting to server...
Job submitted to server.
Manage your jobs at <https://prover.certora.com>.
Follow your job and see verification results at <https://prover.certora.com/output/{job_id}/{unique_key}>.

Verifying Pre-Built Contracts

To run the Certora Prover using the “verifying pre-built contracts” configuration:

certoraSolanaProver prebuilt_config.conf

Expected Output:

Connecting to server...
Job submitted to server.
Manage your jobs at <https://prover.certora.com>.
Follow your job and see verification results at <https://prover.certora.com/output/{job_id}/{unique_key}>.

Building Projects

The cargo certora-sbf command compiles the project and prepares it for verification, passing all the relevant metadata to the Prover. Some additional information has to be specified by the user in the Cargo.toml file in the [package.metadata.certora] section. For instance, the list of source files that have to be uploaded can be specified as follows:

sources = [
    "Cargo.toml",
    "src/**/*.rs"
]

For a complete example, see Cargo.toml in the SolanaExamples repository.

The command cargo certora-sbf offers various CLI options. For instance, the --json option will print the result of the compilation in JSON format. To see the complete list of command line options for cargo certora-sbf run cargo certora-sbf --help.