The Certora Solana Prover

The Certora Solana Prover allows formal verification of Solana smart contracts written in Rust.

Verification rules are written in CVLR (Certora Verification Language for Rust), an embedded DSL that lives in two crates:

• cvlr — core verification primitives (#[rule], cvlr_assert!, cvlr_assume!, nondet, clog!, the Nondet and CvlrLog derives, CvlrFormula / cvlr_lemma! / cvlr_spec! / cvlr_rules! for the spec layer, mock_fn, cvlr_hook_on_exit, …).

• cvlr-solana — Solana-specific helpers (nondeterministic AccountInfo, Pubkey, anchor account wrappers, clock helpers).

The recommended starting scaffold for new projects is the Certora Solana spec template — it ships the canonical run.conf, the baseline inlining / summaries files, and a setup script that wires everything into your Cargo.toml. The pages below assume the layout that template produces.

The pages below are organized so that you can read top-to-bottom for a full walkthrough, or jump directly to the topic you need.

Setup and tooling

• Get started with the Solana Certora Prover
• Using the Solana Certora Prover
• Solana-Specific Options / CLI Flags
• Understanding Prover Output for Solana Programs
• Rule Sanity Checks (Solana)
• Troubleshooting

Writing specifications

• Certora Verification Language for Rust (CVLR)
• Nondet & Havoc
• Specifications and Lemmas
• Mocks & Feature Gates
• Solana Accounts
• Anchor
• Parametric Rules & Macros
• Methodology