#[derive(VerifiedAccounts)].Verified Anchor is a formally verified, drop-in replacement for Anchor's #[derive(Accounts)] — the macro that gates account validation on nearly every Solana program. Every macro expansion ships with a build-time Lean 4 proof that the generated Rust validator implements a precise validation contract (signer, mut, owner, has_one, seeds/bump, discriminator, init/close), so the build fails unless the validation is proven. This eliminates the macro-level account-validation bug class — Cashio, Crema, type confusion, PDA misuse — by construction, with a single dependency: cargo add verified-anchor.
Three commands. No clone, one dependency.
It is published on crates.io. Add it, install the proof gate, and check — the checker fetches the pinned Lean proofs itself on first run (you only need elan / lake, the Lean kernel, to verify a proof). No repository clone, no --lean-dir.
$ cargo add verified-anchor # runtime + the proof macros — the only dependency $ cargo install cargo-verified-anchor # the build-time proof gate
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>, } verified_anchor::emit_specs!(); // one line — lets `check` discover your structs
$ cargo verified-anchor check ✓ Transfer (validation) All 1 proof obligation(s) discharged.
Everything — Pubkey, AccountInfo, ProgramResult, declare_id!, the wrappers, the derives — comes from the single verified-anchor crate. No separate solana-program or borsh.
A drop-in replacement for Solana's #[derive(Accounts)] macro — with proofs attached.
Anchor is the framework almost every Solana program in production is built on. When you describe accounts in a struct ("this one must sign, this one must be writable, this one must be a PDA derived from these seeds…"), Anchor generates the checking code at compile time and your program runs those checks on every Solana transaction — before any lamport movement, before any business logic, before anything. That generating code itself has never been formally verified. A bug there is a bug in every Anchor-based Solana program in production.
Verified Anchor is the same framework, with the same Anchor-style syntax (Account<'info, T>, Signer<'info>, Program<'info, P>, Context<T>), except every macro expansion comes with a Lean 4 proof that the generated check is equivalent to a contract that defines what "valid accounts" means in the Solana account model. The user writes the same Solana program code. The proof is checked at build time. If it does not check, the program does not compile.
The Lean library models concrete Solana primitives — the real findProgramAddress PDA derivation, lamports, rent, owner and executable flags — under the VerifiedAnchor.Solana namespace, designed to compose with the broader Solana formal-methods stack (QEDGen.Solana, lean_solana). Runtime tests compile to SBF via cargo-build-sbf and execute on litesvm, an in-process Solana VM.
The silent gap in Solana's correctness chain.
Solana's correctness depends on a chain of trust. Layers 1, 2, and 4 receive substantial attention from the Solana ecosystem. Layer 3 — Anchor's macro expansion, which gates almost every Solana transaction in production — does not. Verified Anchor closes that layer.
#[derive(Accounts)] macroAnchor is universal Solana infrastructure. A class of bug eliminated at the framework level is a class eliminated across the ecosystem. The Lean library composes directly with QEDGen.Solana: Verified Anchor proves account validation; QEDGen proves business logic; together they give Solana an end-to-end proof story no other major blockchain currently offers at the framework level.
Over $50M lost on Solana mainnet to one family of bug.
Solana programs have lost — and continue to lose — large sums of money to attacks that are not exotic. They are variations on the same theme: the program thought it was checking an account, but the check was either missing, malformed, or trivially bypassable. This is exactly the class of bug Anchor's #[derive(Accounts)] is supposed to prevent. The reason the framework does not is that the framework itself is unverified. Four examples, all real Solana mainnet incidents, all reproduced in this repository as before-and-after litesvm tests:
bank field matched the bank account passed in the same instruction. Attacker passed a forged collateral account whose bank field pointed at an attacker-controlled mint.Same syntax as stock Anchor. The proof comes free.
If you have used Anchor, you already know how to use Verified Anchor. The wrapper types, the attribute macros, the Context<T> shape — all signature-identical to stock Anchor. The only thing that changes is what happens at build time.
use anchor_lang::prelude::*; #[account] pub struct Vault { pub authority: Pubkey, pub amount: u64, } #[derive(Accounts)] pub struct Transfer<'info> { #[account(mut, has_one = authority)] pub vault: Account<'info, Vault>, pub authority: Signer<'info>, }
use verified_anchor::prelude::*; #[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>, }
The only diff is one identifier. Both compile to runtime checks that look the same. The verified-anchor version additionally emits a Lean obligation that a checker (run via cargo verified-anchor check) discharges against the proven library.
Install from crates.io — no clone required. The check command fetches the pinned proof library itself on first run; you only need the Lean toolchain (elan) present.
$ cargo add verified-anchor # runtime + the proof-producing macros $ cargo install cargo-verified-anchor # the build-time proof gate $ cargo verified-anchor check # discharges every struct's obligation via Lean
A single struct flows into both the Rust check and the Lean obligation.
The macro emits the Rust check and a Lean obligation from the same struct description. The Rust check runs on chain at transaction time. The Lean obligation is discharged at build time against the proven library. Both are observably equivalent by construction.
#[derive(VerifiedAccounts)].validate() function, (b) a Lean AccountsStruct literal describing the same constraints.genValidate on AccountsStruct. The same struct literal flows into the Rust check and into genValidate — they iterate the same constraints in the same order.genValidate s c = true ↔ validates s c. The generated checker is equivalent to the validation contract. Proven once, for all structs.cargo verified-anchor check runs lake env lean and discharges a per-struct obligation by decide M4Subset. If the obligation fails, the build fails.theorem genValidate_sound
(s : AccountsStruct) (c : Ctx) (h : M4Subset s) :
genValidate s c = true ↔ validates s c
For every struct in the supported subset, the generated Rust validator returns Ok(()) exactly when the declarative contract holds. Proved once, parameterised over the user's struct. The lifecycle theorem lifecycle_sound discharges analogous Hoare obligations for init and close. Both depend only on [propext, Quot.sound].
Two commands. No assumptions required.
The proofs are open. 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.
Clone the repository, install elan and lake, then:
$ cd lean && lake build $ lake env lean Audit.lean
'VerifiedAnchor.genValidate_sound' depends on axioms: [propext, Quot.sound]
The same audit applies to lifecycle_sound (the init and close Hoare theorem). Same answer.
The trust boundary, in full.
The library's claim is not that Solana programs become bug-free. The claim is that the macro-level account-validation bug class — the class that ate Cashio, Crema, and the type-confusion incidents — is eliminated at the framework level for the supported constraint subset.
signer, mut, owner, has_one, seeds + bump, discriminator. Plus the init / close lifecycle as a Hoare theorem.
Borsh deserialisation of typed payloads (BorshFailed is an honest runtime error, not a silent gap). CPI effects beyond init / close. The Solana runtime contract itself.
realloc, zero, token / mint / associated-token, custom constraint = expr. The macro emits a compile_error! with a migration-guide pointer.
Four real Solana mainnet CVE classes are reproduced as litesvm before-and-after tests. Naive version: attacker wins. Verified version: attacker rejected on chain.
Documentation for reviewers, contributors, and users.