SPECTRE
Research
Methodology2026-05-16

SPECTRE × Certora SCP — FV Integration Design

Author: spectre-solana-max engineering Status: Design doc. PoC implementation deferred to a follow-up. Companion: spectre-vs-competitors-gap-analysis-2026-05-16.md (tier-3 item 7).

Premise

SPECTRE and the Certora Solana Prover (SCP) live at orthogonal layers of the security stack:

Layer SPECTRE Certora SCP
Analysis unit architectural patterns across a codebase per-function logic against a written specification
Output "your handler shape matches incident class X" "this handler provably satisfies invariant Y" or "here is a counter-example"
Setup cost zero — point at a repo, scan hours-to-days per verified property (CVL harness + abstractions)
Strength survey breadth, regression detection formal proof, exact counter-examples

They compose: SPECTRE flags the suspicious patterns; Certora proves (or disproves) the specific invariants those patterns gate. The friction today is harness authorship: writing a CVL spec from scratch takes hours. SPECTRE has structured knowledge of every handler's accounts struct, predicates, mutated fields, and CPI shape — much of what a CVL harness needs.

Integration shape

Three components, in increasing scope:

Component 1: pinpoint spectre certora-skeleton <handler> (1-2 days)

A new CLI subcommand that consumes SPECTRE's symbol-table output and emits a starter Certora CVL harness file for a named handler. Pre-fills:

  • Accounts struct → CVL methods { } block. Each Anchor Account<'info, T> field becomes a CVL declaration with the right type.
  • #[account(...)] constraints → CVL preserved clauses. has_one, seeds = [...], constraint = ... translate to preserved invariants.
  • Mutated fields → CVL ghost declarations. Pulled from FieldMutationIndex.
  • CPI calls → CVL summarize directives. Each CPI gets a NONDET summary by default; the human refines.
  • Handler precondition skeleton. From the predicates we already extract for ARI-040 / RACE-001 / etc.

Output is a working-but-trivial CVL file. The human adds the actual invariants (the load-bearing per-engagement work) and runs certoraRun. The skeleton saves the boilerplate, not the proof.

Component 2: Finding-driven invariant suggestions (~1 week)

When a SPECTRE rule fires, attach a CVL invariant template. Example: RACE-001 emits "handler reads ctx.accounts.vault.amount after CPI without reload" — the attached invariant template is rule cpi_invalidates_amount { ... assert lastReverted || vault.amount == old(vault.amount); ... }. Each rule gets a hand-written template; the CLI substitutes the handler / account / field names.

This builds a per-rule library of "if this rule fires, here is the FV spec that would prove it absent".

Component 3: Continuous-FV mode (~3 weeks, requires Certora Pro)

pinpoint spectre fv-watch — for each new SPECTRE finding in CI, automatically generate the harness from Component 1 + Component 2, run certoraRun, and surface the result in PR annotations. The dev gets a SPECTRE finding and a Certora proof obligation in the same PR. Either fix the code, prove the invariant, or document acceptance.

Why this is high-leverage

  • SPECTRE-only: catches patterns, can't prove absence.
  • Certora-only: requires hand-written specs for every property, scales poorly.
  • Combined: SPECTRE's pattern detection becomes the entry-point for Certora's proof obligation. The user writes ONE invariant per rule-class instead of per-protocol; the harness skeleton is auto-generated.

The cost is mostly glue and templates. The hard part (the prover) is already open-source and production-grade.

Concrete next steps

  1. Phase 1 (1 day): Add pinpoint spectre certora-skeleton --handler <name> subcommand. Stub the CVL output.
  2. Phase 2 (3 days): Wire FieldMutationIndex + accounts-struct fields + CPI shape into the skeleton generator. Validate the skeleton compiles under certoraRun --typecheck.
  3. Phase 3 (1 week): Per-rule invariant templates for the 10 highest-frequency rules (ACC-010/011/013, RACE-001, INV-001/004, CPI-020, AUTH-100, GOV-001, ITER-001).
  4. Phase 4 (3+ weeks): fv-watch continuous mode with Certora API integration.

Scope boundary

Phase 1 ships standalone CLI value: a dev can run pinpoint spectre certora-skeleton and get a working starter file, even without continuous integration. That's the minimum viable integration.

The full continuous-FV mode (Phase 4) is gated by Certora Pro subscription cost and is a separate sales conversation. The substrate work (Phases 1-3) is independent of that.

References