#solana #certora #formal-methods #assert #verification

app cargo-certora-sbf

Build a program for Certora Verification using Certora's version of Solana Platform Tools

3 unstable releases

new 0.3.1 Apr 18, 2025
0.3.0 Apr 17, 2025
0.2.0 Apr 4, 2025

#60 in Debugging

Download history 90/week @ 2025-03-30 44/week @ 2025-04-06 286/week @ 2025-04-13

420 downloads per month

Apache-2.0

40KB
720 lines

cargo-certora-sbf

A Cargo subcommand that integrates Certora formal verification into Rust-based Solana BPF (SBF) smart contract development workflows.

πŸ“¦ Installation

Requirements

  1. rustup installer for Rust
  2. Rust version >= 1.81 to compile cargo-certora-sbf itself
  3. (optional) Solana CLI version >= 1.18
  4. (optional) Rust version v1.75. This version corresponds to Rust bundled with Solana v1.18.
  5. (optional) Rust version v1.79. This version corresponds to Rust bundled with Solana v2.1

Instructions

Install via cargo install:

cargo install cargo-certora-sbf

Ensure you have Rust installed using rustup. cargo-certora-sbf requires Rust version 1.81 or higher.

πŸš€ Usage

Use from the command line just like any other cargo subcommand:

cargo certora-sbf [OPTIONS]

πŸ”§ Options

Run cargo certora-sbf --help for the full list of options.

πŸ›  How It Works

cargo-certora-sbf automates:

  • Managing Certora Solana Platform Tools (includes a Rust compiler version enhanced for Certora Prover compatibility).
  • Compiling Solana smart contracts into a form suitable for formal verification.

FAQ

  1. How to resolve the error "... cannot be built because it requires rustc 1.79.0 or newer"

    This error typically occurs when you intend to use Solana v1.18, but cargo decided to use Solana v2 or above. This usually happens when Rust with version >v1.75 is used to configure the project to create or update Cargo.lock. This, in turn, most often happens by rust-analyzer in VSCode automatically configuring the project when it is first opened.

    To resolve, first undo by restoring or removing Cargo.lock. Then, configure using Rust v1.75. For example, simply running

    cargo certora-sbf
    

    should work.

    To investigate further, run check subcommand manually (but use Rust v1.75!)

    cargo +1.75 check
    
  2. How to use cargo-certora-sbf with projects that require Solana v2 (that require Rust v1.79)

    This requires platform-tools version v1.43 or above. Use

    cargo certora-sbf --tools-version v1.43
    
  3. If you get an error message like below:

    error: not a directory: '/Users/some_user/.local/share/solana/install/active_release/bin/sdk/sbf/dependencies/platform-tools-certora/rust/bin'
    [ERROR] execution of "rustup" terminated with exit status: 1
    

    try reinstalling via cargo certora-sbf --no-build --force-tools-install.

  4. Is it possible to install platform tools without building a rust project.

    Yes. Use the following command line flags:

    cargo certora-sbf --no-build --force-tools-install
    
  5. Something is not working, how to get more information on what is going on?

    Enable extra verbosity by using -vv flag.

πŸ“„ License

Apache 2.0. See LICENSE for details.

πŸ™Œ Contributions

Issues, pull requests, and feedback are welcome!

βΈ»

Made with ❀️ by Arie Gurfinkel for Certora

Dependencies

~14–30MB
~512K SLoC