QEDGen

---

Write what your Solana program must guarantee in a .qedspec file. QEDGen validates the spec, finds bugs your tests miss, then generates the verification artifacts and implementation scaffold needed to keep them fixed: property tests, Kani harnesses, Lean 4 proofs, agent-fill program scaffolds, and CI workflows — all from a single source of truth. Frameworks: Anchor, Quasar, and Pinocchio (greenfield scaffold via qedgen init --target ...), plus sBPF assembly through the dedicated Lean/qedsvm proof path. Brownfield source audit covers Anchor / Quasar / Pinocchio / native Rust via qedgen probe (with Miri-backed UB detection for Pinocchio) and lifts findings into a ratifiable spec. The auditor does not audit sBPF assembly; use qedgen asm2lean or a .qedspec for that target.

Alpha: expect bugs and breaking API changes while the project evolves.

npx skills add qedgen/solana-skills

Installing the CLI is a separate, explicit step. From the installed qedgen skill directory:

bash install.sh --link-dir "$HOME/.local/bin"   # drop --link-dir to skip the PATH link
qedgen --help

--link-dir is what makes the bare qedgen in every example below resolve; make sure that directory is on your PATH. Without it the CLI installs only into the skill's own bin/, and you run it as tools/qedgen from the skill directory. See installation, upgrades, and prerequisites.

Already installed? Skills CLI 1.7.0 and newer migrates the skill's new runtime layout during an ordinary update. With Skills CLI 1.5.9, upgrade the client or explicitly re-add it with npx skills add qedgen/solana-skills --skill qedgen. Either replacement removes the locally installed QEDGen binary, so enter the installed qedgen skill directory and rerun bash install.sh. See the linked guide for exact migration steps and the optional auditor-hook change.

Works with Claude Code, Cursor, Windsurf, GitHub Copilot, and any agent supporting the Agent Skills spec.

Or just point your agent here. Paste this to your coding agent and it installs QEDGen and gets to work:

Set up QEDGen for this program — follow https://qedgen.dev/llms-full.txt

That page opens with a Quickstart for agents (install, then audit your existing program or write a .qedspec from scratch), followed by the full reference. The shorter qedgen.dev/llms.txt is the index version.

How it works

.qedspec ──► check (lint/report) ──► codegen --all ──► agent fill ──► verify ──► ∎
                │                         │                 │          ▲       │
                ├── lint (instant)        ├── Rust scaffold  │          ├─► Leanstral (fast)
                ├── coverage matrix       ├── Lean stubs     │          └─► Aristotle (deep)
                └── drift reports         ├── Kani harnesses └── cargo/lake/proptest
                                          └── tests + CI

1. Define guarantees — write a .qedspec describing what your program must guarantee, or let your agent generate one from the code or IDL
2. Validate — qedgen check runs spec lint, coverage, drift checks, and reports; run generated proptest/Kani/Lean backends with qedgen verify
3. Generate — qedgen codegen --all produces test harnesses, Lean stubs, CI workflows, and an agent-fill Rust scaffold from the single spec
4. Prove — your agent fills proof obligations; Leanstral handles routine sub-goals (seconds), Aristotle handles the hardest ones (minutes–hours)

What it verifies

Property	Approach
Access control	Signer checks, authority constraints
CPI correctness	Correct program, accounts, flags, and discriminator for each invocation (axiomatic, pure rfl)
State machines	Lifecycle correctness, one-shot safety
Conservation	Named invariants and propertys preserved (or establishes-ed) across operations. Per-handler proptest + Kani harnesses fire when the body has a Rust rendering; Lean theorems back the proofs.
Fuzz-discovered paths	Coverage-guided fuzzer (qedgen codegen --crucible + qedgen probe --fuzz) drives the deployed .so with mutated typed-action sequences. Crashes auto-tmin to minimal reproducers, dedupe by (handler, outcome), and surface via qedgen verify --crucible with action-sequence counterexamples.
Arithmetic safety	Overflow/underflow for fixed-width integers, U64 bounds
Input validation	Account count, duplicates, data length, discriminators, parameter bounds — each guard maps to a specific error exit
Memory correctness	Stack/heap disjointness, pointer arithmetic (sBPF)
Pinocchio soundness	unsafe-serde and arithmetic site catalogue via qedgen probe --program <root>; qedgen verify --miri runs the generated repros under cargo +nightly miri test and surfaces UB / aliasing / overflow plus Miri-fail / Mollusk-pass divergence as Critical findings.
PDA integrity	Program-derived address derivation and 4-chunk comparison (sBPF)
Deploy safety	On-chain shape for Anchor and Quasar programs — version fields, reserved padding, pinned discriminators, signer coverage, PDA seed continuity — via qedgen readiness and qedgen check-upgrade (ratchet).

CPI calls are axiomatic — we verify the program passes correct parameters. SPL Token internals and the Solana runtime are trusted.

Proofs prove correctness. Ratchet proves deployability. The P-rule preflight (qedgen readiness) catches future-upgrade risks in a single IDL before the first deploy; the R-rule diff (qedgen check-upgrade) catches every breaking change between an old and new IDL once the program is live.

Quick start

# 1. Install
npx skills add qedgen/solana-skills

Two paths from here — pick the one that matches what you have:

This is the beginning of the README. Read the rest at the original. Read the full README ↗