Formal Verification

Formal Verification

Certora Sunbeam checks selected protocol properties against a model of the contracts. Formal verification complements Testing and Quality and security review; compilation or a successful job submission does not establish a proof result.

A verdict applies to the exact artifact, configuration, and assumptions in its report. A timeout, skipped rule, or tooling error leaves the property unproved for that run.

What the rules cover

Rules are grouped by the component whose behavior they check. Each group has focused rule modules, fixtures, and prover configurations under certora/.

Area	Properties under review
common	Fixed-point bounds, rounding, interest, and valuation arithmetic.
pool	Shares, indexes, cash, revenue, settlement, fees, and flash accounting.
controller	Account isolation, solvency gates, position actions, liquidations, and strategies.
price-aggregator	Price-source admission, freshness, tolerance, caching, and fail-closed behavior.
Shared summaries	Assumptions about cross-contract behavior used by other rules.

Protocol Invariants describes the required properties. A rule proves only the property it expresses within its modeled domain; a directory or profile name is not a claim of complete coverage.

Understand the proof boundary

Pool rules exercise accounting transitions before token transfers. They do not model arbitrary token behavior, callbacks, allowances, reentrancy, or transaction rollback.

Controller rules use summaries for some pool, oracle, token, and external calls. A result that relies on a summary is conditional on that summary's correctness. Controller valuation rules assume an accepted price unless the rule explicitly models price failure.

Loop bounds and fixture preconditions also limit the result. Arbitrarily long batches and accrual periods are not covered merely because bounded examples prove. Check these assumptions before treating a verdict as evidence for a protocol change.

Check and build the proof artifacts

Run commands from the repository root. The local compilation checks do not invoke the SMT prover:

./certora/compile_all.sh

The script checks the four certora feature paths and their focused variants. It also checks rule/configuration alignment and the mapping from configurations to focused WASM artifacts.

Build and verify artifacts before submitting proofs:

./certora/compile_all.sh --wasm

This adds make certora-wasm and the artifact-integrity checker. To rebuild only the prover artifacts and check their provenance:

make certora-wasm
python3 certora/scripts/check_wasm_artifacts.py

Focused WASM lives under artifacts/wasm/certora/. Each artifact includes a focused rule module and preserves function names; the build disables the Stellar optimizer. The manifest binds artifacts to their source fingerprints and feature sets.

Rebuild after changing contracts, rules, fixtures, summaries, or relevant dependencies. Deployment artifacts under artifacts/wasm/deploy/ serve a different purpose and cannot replace focused prover artifacts.

Select a proof profile

Profiles in certora/profiles.json group configurations by purpose. List or inspect them before running a campaign:

./certora/scripts/run_profile.py --list
./certora/scripts/run_profile.py sanity --dry-run

Profile	Scope
sanity	Reachability witnesses, including witnesses for rejection-rule fixtures.
fast	Arithmetic, rates, valuation, and lighter safety properties.
core	Stateful solvency, liquidation, strategy, pool accounting, and price-system rules.
heavy	Selected rules with larger proof budgets.
flash-position	Focused flash-position success, rejection, and reachability rules.
manual	core plus heavy.
all	sanity, fast, core, and heavy.

Start with the relevant reachability checks, then run the rules that cover the changed behavior. Profile names describe selection, not completion time or proof status.

Run the prover

Hosted execution requires the Certora CLI and a CERTORAKEY environment variable. After building and checking the artifacts, submit a profile and wait for results:

./certora/scripts/run_profile.py sanity -- --wait_for_results ALL

Extra arguments after -- reach every configuration in the profile. Run a single rule from its own configuration rather than passing that rule name to an entire profile:

cd certora/common/confs
certoraSorobanProver math.conf --rule ray_mul_identity_native --wait_for_results ALL

A local prover installation needs a compatible Java runtime, Certora CLI dependencies, and the local prover binaries. From the repository root:

./certora/scripts/run_profile.py sanity --local

Use the repository Certora guide for local installation, resource settings, and troubleshooting. Increasing a timeout alone does not resolve a missing model, an unreachable fixture, or an invalid assumption.

Interpret results and sanity checks

Universal assertions and reachability witnesses answer different questions. An assertion checks a property across the modeled inputs; a satisfy witness shows that a path can complete. A witness does not prove the corresponding universal property.

The configurations use rule_sanity: advanced for assertion rules. On the Sunbeam WASM flow, basic does not run the vacuity check. Satisfy rules use none because the witness itself demonstrates reachability.

Rejection rules also use none: a rule that succeeds only by reverting has no successful exit for the ordinary vacuity check. These rules require a companion witness that shows the fixture can complete. check_orphans.py enforces the configured witness relationship.

For each result, record the source revision, artifact identity, configuration, rule, verdict, and report. Review assumptions and any counterexample. Distinguish a property violation from a loop-unwind failure, timeout, or prover transformation error before changing production code or weakening a rule.

CI coverage

The local prover workflow runs on matching changes to formal rules, shared code, contract source, or the root Cargo manifests. It runs a selected regression set, reports timeouts as warnings, and can skip proof execution when the runner lacks the local prover installation. A green workflow therefore requires inspection of its summary before it counts as proof evidence.

Hosted workflows run on manual dispatch. certora-verification.yml uses the sanity profile when its profile input is empty; selecting a profile creates one job per configuration and rule. These jobs wait for results and record verdicts and report links. No complete hosted profile runs automatically on every pull request.

Sources and related pages

• Certora guide, profiles, and local checks.
• Local prover workflow and hosted prover workflow.
• Protocol Invariants and Security describe the properties and trust boundaries that proof evidence supports.