Verified Anchor

Formally verified account validation for Solana programs.

Verified Anchor is a drop-in replacement for the Anchor #[derive(Accounts)] macro that gates almost every Solana transaction in production. The macros emit the same Rust validation code stock Anchor would emit, plus a Lean 4 obligation discharged at build time against a contract that defines what "valid accounts" means in the Solana account model. The proven core covers signer / mut / owner / has_one / seeds + bump / discriminator, the typed-wrapper base checks (SystemAccount ownership, Program<P> executable + address), and the init / close lifecycle.

Why

Solana's correctness depends on a chain of trust: validator runtime (Agave, Firedancer), SBF execution, the Anchor macro that generates per-instruction account validation, and the program's business logic. Layers 1, 2, and 4 receive substantial attention. Layer 3 — the Anchor macro — has not. It is hundreds of lines of procedural-macro code that has never been formally verified, and a bug in it is a bug in every program that depends on it.

The cost of leaving that layer unverified is measurable. Four real Solana mainnet exploits — Cashio (March 2022, ~$48M), Crema Finance (July 2022, ~$8.8M), account-type confusion incidents, and PDA seeds misuse — share the same root cause: a check the program thought it was making was either missing, malformed, or trivially bypassable. Each of these is exactly what #[derive(Accounts)] is supposed to prevent.

Verified Anchor closes the gap. Every macro expansion ships with a Lean 4 theorem stating that the generated Rust validator is observably equivalent to a contract written in Lean. The theorem is proved once, parameterised over the user's struct. The user writes the same code they would write in stock Anchor. The four CVE classes above are reproduced in this repository as before/after litesvm tests; the verified versions reject the attacker on chain.

Status

• v0.1.2, published on crates.io — one dependency: cargo add verified-anchor. v0.1.0 is the tagged submission snapshot.
• Lean theorems' axioms: [propext, Quot.sound] only. Zero sorry / admit.
• Out of scope: realloc, zero, token / mint / associated-token constraints. Custom constraint = ... expressions. QEDGen composition demo.

Packages

Repo structure

lean/                                 Lean 4 library (lake build)
  VerifiedAnchor/Solana/              Solana account model + crypto (opaque sha256, isOnCurve)
  VerifiedAnchor/Constraints/         Constraint AST (the Rust↔Lean seam) + Ctx
  VerifiedAnchor/Contract/            `validates : AccountsStruct → Ctx → Prop`
  VerifiedAnchor/Decision/            `validatesBool` + agreement theorem
  VerifiedAnchor/Codegen/             `genValidate` + soundness proofs (Soundness, Lifecycle)
  VerifiedAnchor/Examples/            Worked example (Withdraw.lean)

rust/                                 Cargo workspace
  verified-anchor/                    Runtime crate (traits, errors, prelude, integration tests)
  verified-anchor-macros/             Proc-macro crate
  cargo-verified-anchor/              Cargo subcommand
  verified-anchor-program/            BPF program — init/close + a seeds PDA (litesvm fixture)
  verified-anchor-example/            Worked user crate
  verified-anchor-exploits/           Empirical exploit suite (four CVE classes)

docs/                                 Project documentation
  verified-anchor-bridge.md           Trust boundary + clause-by-clause Rust↔Lean correspondence
  migrating-from-anchor.md            Migration guide + supported constraint subset
  exploit-case-studies.md             The four Solana mainnet incidents, reproduced before/after
  announcement-v0.1.0.md              v0.1.0 release writeup
  publish-checklist.md                crates.io release steps

web/index.html                        Self-contained landing page (deployable on GitHub Pages)
verified_anchor_proposal.md           Original proposal
LICENSE                               CC BY-NC-ND 4.0

Documentation

• Original proposal — problem statement, approach, milestones.
• v0.1.0 announcement post — the full technical writeup.
• Trust boundary — what is proven, what is not, the Rust↔Lean correspondence.
• Migrating from Anchor — supported constraint subset, syntax mapping.
• Exploit case studies — four Solana mainnet incidents reproduced on litesvm.

Quick start

Install from crates.io — no clone required:

cargo add verified-anchor             # runtime + the proof-producing macros
cargo install cargo-verified-anchor   # the build-time proof gate

Then write the same code you would in stock Anchor:

use verified_anchor::prelude::*;

declare_id!("YourProgram1111111111111111111111111111111");

#[account]
pub struct Vault {
    pub authority: Pubkey,
    pub amount: u64,
}

#[derive(VerifiedAccounts)]
pub struct Transfer<'info> {
    #[account(mut, has_one = authority)]
    pub vault: Account<'info, Vault>,
    pub authority: Signer<'info>,
}

pub fn transfer<'info>(program_id: &Pubkey, accounts: &'info [AccountInfo<'info>], data: &[u8]) -> ProgramResult {
    let (ctx, _bumps) = Transfer::try_accounts(program_id, accounts, data)?;
    let _amount = ctx.vault.amount;
    // your handler logic
    Ok(())
}

// One line, anywhere in your crate's lib — lets `cargo verified-anchor check` discover the structs.
verified_anchor::emit_specs!();

The whole prelude (Pubkey, AccountInfo, ProgramResult, declare_id!, the wrappers, the derives) comes from the single verified-anchor dependency — no separate solana-program or borsh. Then discharge the per-struct proof obligation (the first run fetches the pinned Lean proof library automatically; you only need elan/lake installed):

cargo verified-anchor check -p my-crate

Deep technical dive

The verification chain

The #[derive(VerifiedAccounts)] macro emits two artefacts from a single source struct:

1. The Rust impl Validate — a validate(accounts, instr_data, program_id) -> Result<(), VAError> function that runs at transaction time. Per field it walks the declared constraints in order and short-circuits on the first failure.
2. A Lean AccountsStruct literal — the same struct, rendered as a value of the Lean type that the proof side consumes.

A Lean function genValidate : AccountsStruct → Ctx → Bool recursively interprets the constraint list. By construction, the Rust validator and genValidate examine the same constraints in the same order and return the same answer on the same input. Equivalence is by construction; the proof side proves equivalence to the contract, not to the Rust.

The contract validates : AccountsStruct → Ctx → Prop is defined declaratively in Lean. It says exactly what each constraint kind means — signer means the slot is a signer, has_one = f means the 32 bytes at offset 8 of the account data equal the key of the named field, seeds = […], bump means the account key is the canonical PDA for those seeds under program_id, and so on.

The headline theorem ties the two together:

theorem genValidate_sound (s : AccountsStruct) (c : Ctx) (h : M4Subset s) :
  genValidate s c = true ↔ validates s c

For every struct in the supported subset (called M4Subset in Lean — see the table below), genValidate returns true precisely when the declarative contract holds. The two sides cannot disagree. The lifecycle theorem lifecycle_sound discharges analogous Hoare obligations for init and close.

Per-program proof obligations are discharged by cargo verified-anchor check. For each user struct the cargo tool generates a one-line Lean obligation decide (M4Subset s), then invokes lake env lean. If the obligation fails, the build fails.

Proof scope

What is proven, what is not

The library's claim is not "your Solana program is now bug-free". The claim is that the macro-level account-validation bug class is eliminated at the framework level for the supported constraint subset. Full discussion in docs/verified-anchor-bridge.md.

Build and test

Lean (4.30.0, via elan; dependency: batteries):

export PATH="$HOME/.elan/bin:$PATH"
cd lean && lake build

Rust workspace (1.93+):

cd rust && cargo test --workspace

SBF programs (requires solana-cli platform-tools):

export PATH="$HOME/.cache/solana/v1.53/platform-tools/rust/bin:$HOME/.local/share/solana/install/active_release/bin:$PATH"
cd rust/verified-anchor-program && cargo-build-sbf --no-rustup-override
cd rust/verified-anchor-exploits && cargo-build-sbf --no-rustup-override

End-to-end proof discharge (Lean + cargo together):

cd rust
cargo run -q -p cargo-verified-anchor -- verified-anchor check -p verified-anchor-example  --lean-dir ../lean
cargo run -q -p cargo-verified-anchor -- verified-anchor check -p verified-anchor-exploits --lean-dir ../lean

Audit the proofs

The headline theorems' axiom dependencies are [propext, Quot.sound], the standard Lean propositional-extensionality and quotient-soundness axioms. No sorry, no Classical.choice, no native_decide.

cd lean
lake env lean Audit.lean                 # prints both headline theorems' axiom sets
grep -rn 'sorry\|admit' VerifiedAnchor/

Examples

• rust/verified-anchor-example — worked user crate exercising validation + lifecycle.
• rust/verified-anchor-exploits — four real Solana mainnet CVE classes, naive vs verified.

Landing page

A self-contained static landing page lives under web/. It uses no build step, no framework, and no external scripts beyond Google Fonts. Preview locally with any static server:

cd web && python3 -m http.server 8000
# then open http://localhost:8000

To host on GitHub Pages:

1. In the repository on GitHub, open Settings → Pages.
2. Under Build and deployment, set the source to Deploy from a branch.
3. Choose Branch: master and Folder: /web. Save.

The site goes live at https://parthrathix0.github.io/Verified-Anchor/ within a minute. A web/.nojekyll file is committed so GitHub Pages serves the file as-is without running it through Jekyll.

Contributing

Issues and audit attempts are welcome. Substantive code patches require a prior contributor agreement granting the author the right to incorporate the change under the project license (see below). Open an issue first if you intend to send code.

License

CC BY-NC-ND 4.0. This is not a standard open-source license. Practical effects:

• NonCommercial. No use for commercial advantage without prior written permission.
• NoDerivatives. No distribution of modified versions.