# QEDGen

> Describe what your Solana program must guarantee in `.qedspec`. QEDGen finds the bugs your tests miss, then generates the proofs, property tests, and CI to keep them fixed. Supports Anchor, Quasar, Pinocchio, and native sBPF assembly. It also audits existing programs (brownfield) with no spec required.

## Quickstart (for agents)

A developer pointed you to this document to set up QEDGen and use it on their Solana program. Do this, in order:

1. **Install.** Run `npx skills add qedgen/solana-skills`, then run `bash install.sh` from the installed skill directory. Set `QEDGEN` to that directory's `tools/qedgen` wrapper and run `"$QEDGEN" --help` to confirm. The wrapper never installs anything; explicitly request a PATH link with `bash install.sh --link-dir "$HOME/.local/bin"` if desired. No API keys are needed for the core loop.
2. **Find out where the developer is, then act:**
   - **Brownfield** (an existing program, no spec) → *audit first.* Run `qedgen probe --program <path>` — it reports real bugs (each with a Kani/proptest/Mollusk reproducer), coverage gaps, and a ranked set of evidence-anchored invariant hypotheses about what the program appears to guarantee. Ask the developer to confirm each hypothesis (accept / reject / it's-a-bug), record the answers to `<audit-dir>/answers.json`, and run `qedgen ratify --audit-dir <dir>` to lower confirmed ones into an executable `.qedspec`. (`qedgen adapt --program` and `qedgen spec --idl` are deprecated TODO-shell scaffolds — this flow subsumes both.)
   - **Greenfield** (defining guarantees for new or evolving code) → write a `.qedspec`, then `qedgen check --spec …` → `qedgen codegen --spec … --all` → `qedgen verify --spec …`.
3. **The `.qedspec` is the single source of truth.** Refine the spec rather than hand-editing generated artifacts.

The rest of this document is the full reference — every CLI command, the proof-writing workflow, the Lean support-library API, proof patterns, and worked examples.

## Installation

```bash
npx skills add qedgen/solana-skills
```

The installer sets up only the CLI binary. Install Rust, Lean/elan and Kani yourself when needed. Explicit `qedgen setup --mathlib` prepares the proof workspace and downloads Mathlib dependencies/cache using your installed Lean tools. No API keys are required for the default workflow (spec writing, validation, code generation).

## What It Does

A `.qedspec` is the single source of truth. It can live in one file or span multiple files with upstream spec dependencies. From it, QEDGen generates program code, property tests, Kani harnesses, Lean 4 proofs, and CI workflows, and keeps them in sync with `#[qed(verified)]` drift detection.

### How It Works

1. **Write the spec.** The agent writes a `.qedspec` describing your program's types, state machines, handlers, guards, effects, and properties. Use one file, split across handler/interface files, or extend an upstream spec.
2. **Validate the spec.** `qedgen check --spec program.qedspec` runs lint, coverage, and drift. Add `--explain` for a Markdown report.
3. **Generate artifacts.** `qedgen codegen --spec program.qedspec --all` produces the program skeleton for your `--target` (Anchor / Quasar / Pinocchio), proptest harnesses, Kani BMC harnesses, Lean 4 proofs, unit tests, and integration tests. (sBPF specs emit Lean proofs only — assembly is verified via Lean + client-side tests, so `--kani` / `--proptest` skip them.)
4. **Verify the implementation.** `qedgen verify --spec program.qedspec` runs every generated harness on disk (proptest, Kani, Lean). Use `--proptest`, `--kani`, or `--lean` to target one backend.
5. **Escalate hard proofs.** Leanstral (`qedgen fill-sorry`) handles routine sub-goals in seconds. Aristotle (`qedgen aristotle submit`) runs agentic proof search for the hardest goals, measured in minutes to hours.

### Supported Agents

Works with Claude Code, Codex, Cursor, Windsurf, and any agent supporting the [Agent Skills](https://agentskills.io) spec.

## CLI Commands

The CLI is the interface between the agent and generated artifacts, not a user-facing tool. The agent drives it; humans edit `.qedspec` files and review diffs.

### Validate a spec

```bash
$QEDGEN check --spec program.qedspec                     # lint + coverage
$QEDGEN check --spec program.qedspec --json              # machine-readable
$QEDGEN check --spec program.qedspec --explain           # Markdown report
$QEDGEN check --spec program.qedspec --drift src/        # drift detection
$QEDGEN check --spec program.qedspec --drift src/ --deep # transitive drift
```

### Generate artifacts from a spec

```bash
$QEDGEN codegen --spec program.qedspec --all                 # everything
$QEDGEN codegen --spec program.qedspec --target pinocchio    # program skeleton (anchor | quasar | pinocchio)
$QEDGEN codegen --spec program.qedspec --lean                # Lean proofs only
$QEDGEN codegen --spec program.qedspec --kani                # Kani harnesses
$QEDGEN codegen --spec program.qedspec --kani-impl           # impl-targeted Kani: real Anchor handler vs symbolic accounts
$QEDGEN codegen --spec program.qedspec --proptest            # proptest harnesses
```

For handlers codegen can't fully mechanize, the agent fills the `todo!()` body directly in-session (no `--fill` verb needed). If it can't, the spec is under-specified — refine and regenerate.

### Run the generated harnesses

```bash
$QEDGEN verify --spec program.qedspec                    # every backend on disk
$QEDGEN verify --spec program.qedspec --proptest         # cargo test --release
$QEDGEN verify --spec program.qedspec --kani             # cargo kani --tests
$QEDGEN verify --spec program.qedspec --lean             # lake build
$QEDGEN verify --spec program.qedspec --json             # machine-readable for CI
```

### Scaffold a new project

```bash
$QEDGEN init                                             # create .qed/ and starter .qedspec
```

### Drift and reconciliation

```bash
$QEDGEN reconcile --spec program.qedspec                 # unified drift report across Rust + Lean
```

### Brownfield: audit an existing program and elicit its spec (no spec required)

```bash
$QEDGEN probe --program ./src                            # bugs + coverage gaps + ranked invariant hypotheses (JSON for the auditor; summary on stderr)
$QEDGEN probe --fuzz 300 --root ./my-program             # Crucible coverage-guided fuzzing (protocol-invariant crash-finder, no spec required)
$QEDGEN interface --idl target/idl/dep.json              # generate a Tier-0 interface block for a CPI dependency
$QEDGEN probe --program ./src --emit-spec-candidates \
  --audit-dir .qed/audit/<id>                           # write the audit working set (skeleton, hypotheses.json, …)
# answer each hypothesis (accept / reject / bug) → .qed/audit/<id>/answers.json, then:
$QEDGEN ratify --audit-dir .qed/audit/<id>               # lower confirmed hypotheses to executable clauses (parse+check gated)
```

`probe` powers the harness-native auditor subagent: it surfaces real vulnerabilities first (each paired with a Kani/proptest/Mollusk reproducer), spec-coverage gaps second, and hypothesizes evidence-anchored invariants (authorization, lifecycle/init-once, held arithmetic bounds, conservation pairs, pinned CPI transfers, unwired error variants, the status-enum state machine) for confirmation. Works on Anchor, native Rust, sBPF, and Pinocchio. Ratified clauses are labelled `checking`; passing generated model proptests are `model-tested`; only source-bound backends earn `implementation-verified`.

Deprecated (functional in v2.x with a warning; removed in v3.0): `qedgen adapt --program` (TODO-shell skeleton) and `qedgen spec --idl` (IDL shell) — the probe flow subsumes both, consuming the IDL as an evidence source.

### Stamp verified handlers (post-verification drift guard)

```bash
$QEDGEN verify --spec program.qedspec --program ./my-anchor-program --kani --kani-path ./my-anchor-program/src/kani_impl.rs
$QEDGEN stamp --program ./my-anchor-program --spec program.qedspec
```

`stamp` (formerly `adapt --program --spec`) emits one `#[qed(verified, …)]` attribute per handler to paste above its `pub fn`; the proc macro recomputes the hashes at compile time and fails the build on drift. It refuses without recorded implementation-verified evidence — a passing Miri run or `kani_impl` harness whose spec and program-source hashes match. Mollusk probe reproducers confirm findings rather than conformance and cannot authorize a stamp.

### Mainnet-readiness (Anchor IDL lint + upgrade-safety diff)

```bash
$QEDGEN readiness --idl target/idl/program.json         # lint one IDL for upgrade-unsafe shapes before first deploy
$QEDGEN readiness --so target/deploy/program.so         # QED002: flag a build older than sBPF v3 (SIMD-0500)
$QEDGEN check-upgrade --old old.json --new new.json     # flag every upgrade-unsafe change between two IDLs
```

### Fill sorry markers with Leanstral (fast, seconds)

```bash
$QEDGEN fill-sorry \
  --file formal_verification/Spec.lean \
  --passes 3 \
  --validate
```

Sends each `sorry` location to the Leanstral model with focused context. Requires `MISTRAL_API_KEY`. (`qedgen generate` is the older whole-proof Leanstral entry point; prefer `fill-sorry`.)

### Escalate to Aristotle (deep, minutes to hours)

```bash
# Submit and wait inline
$QEDGEN aristotle submit --project-dir formal_verification --wait

# Or submit, detach, and poll later
$QEDGEN aristotle submit --project-dir formal_verification
$QEDGEN aristotle status <project-id> --wait --output-dir formal_verification
```

Aristotle runs agentic proof search and returns the project with sorry markers filled. `status --wait` polls periodically and auto-downloads the result on completion. Requires `ARISTOTLE_API_KEY`.

### Transpile sBPF assembly to Lean

```bash
$QEDGEN asm2lean --input src/program.s --output formal_verification/Program.lean
```

Generates a Lean module with `@[simp] def prog`, chunked `progAt` for large programs, `Int`-typed offsets, named constants, and auto-generated `ea_*`, `bridge_*`, and `insn_*` simp lemmas. Designed for the `wp_exec` one-shot tactic.

### Discharge a spec effect against the compiled binary (qedgen ↔ qedsvm seam)

```bash
$QEDGEN descriptor --spec program.qedspec --handler increment   # emit the name-level refinement descriptor (JSON, stdout)
$QEDGEN discharge --spec program.qedspec --handler increment \
  --so target/deploy/program.so --qedlift <path-to-qedlift>    # prove the handler's effect against the compiled bytes
```

`discharge` is the one-command driver over the seam: it builds the descriptor from the `.qedspec`, then discharges it against the `.so` via qedsvm's `qedlift` (built with `--features qedrecover`). Currently covers single-field `+= <int literal>` effects; field offsets resolve from the IDL on the qedsvm side.

### Consolidate proofs

```bash
$QEDGEN consolidate \
  --input-dir /tmp/proofs \
  --output-dir formal_verification
```

### Set up the global validation workspace

```bash
$QEDGEN setup
```

First-time Mathlib build takes 15-45 minutes. Subsequent builds reuse the cache.

### Report a toolchain failure

```bash
$QEDGEN feedback                                         # file a GitHub issue with the last failure's context
```

Bundles the qedgen version, OS/arch, detected runtime, the last command's stderr, and the relevant `.qedspec` excerpt; previews the issue and asks for confirmation before filing.

## Proof-Writing Workflow (SKILL.md)

The skill instructs your agent to follow this workflow:

### Step 1: Understand the program

Check for existing artifacts:
1. **`.qedspec` exists.** Read it. It is the source of truth.
2. **Source (and/or an IDL) exists, no spec.** Run `qedgen probe --program <path> --emit-spec-candidates --audit-dir .qed/audit/<ts>` — the probe consumes the IDL as an evidence source and hypothesizes confirmable invariants; confirmed answers ratify into a draft spec. (`qedgen spec --idl` is the deprecated shell-only fallback.)
3. **Neither exists.** Read source directly, ask scoping questions, then write a draft spec.

### Step 2: Write the spec

The `.qedspec` declares types, state machines, handlers (with auth, accounts, requires, effects, transfers, emits), and properties. It can live in a single file or be split across handler and interface files with upstream dependencies pinned in `qed.lock`.

### Step 3: Validate

Run `qedgen check --spec program.qedspec`. The lint + coverage + drift report tells the agent whether the spec is well-formed and complete.

### Step 4: Generate artifacts

Run `qedgen codegen --spec program.qedspec --all`. This produces:
- Program skeleton for the chosen `--target` (Anchor / Quasar / Pinocchio; default Anchor)
- `tests/proptest.rs` proptest harness
- `tests/kani.rs` Kani BMC harness
- `formal_verification/Spec.lean` (generated, regenerated on every codegen)
- `formal_verification/Proofs.lean` (user-owned preservation proofs, bootstrapped once)
- `.github/workflows/verify.yml` CI

### Step 5: Fill remaining handler bodies (if any)

For handlers where codegen could not fully mechanize the effect (events, token transfers, complex effect RHS), the generated handler carries a `todo!()`. The agent fills the body directly in-session from the spec's declared schema — no separate `--fill` verb. If a body can't be filled, the spec is under-specified: refine it and re-generate.

### Step 6: Verify

Run `qedgen verify --spec program.qedspec`. Proptest runs `cargo test --release`, Kani runs `cargo kani --tests`, Lean runs `lake build`. Failures surface verbatim with summarized diagnostics.

### Step 7: Escalate hard proofs (if any)

```bash
# Fast: Leanstral (seconds)
$QEDGEN fill-sorry --file formal_verification/Spec.lean --validate

# Deep: Aristotle (minutes to hours), when Leanstral fails after multiple passes
$QEDGEN aristotle submit --project-dir formal_verification --wait
```

Always prefer spec refinement over proof shelling. A DSL feature that eliminates the proof obligation structurally is better than a new proof template.

## Support Library API

### Solana (Rust/Anchor)

After `import QEDGen.Solana` and `open QEDGen.Solana`:

**Types:** `Pubkey` (4-chunk LE struct: c0, c1, c2, c3), `U64` (= Nat), `Account`, `Lifecycle` (open | closed), `AccountMeta`, `CpiInstruction`

**Constants:** `TOKEN_PROGRAM_ID`, `SYSTEM_PROGRAM_ID`, `U8_MAX`, `U16_MAX`, `U32_MAX`, `U64_MAX`, `U128_MAX`

**Functions:** `findByKey`, `findByAuthority`, `canWrite`, `closes`, `valid_u64`; CPI predicates `targetsProgram`, `hasDiscriminator`, `hasNAccounts`, `wellFormed` (all rfl-provable on concrete `CpiInstruction` values)

**Key lemmas:** `closes_is_closed`, `closes_was_open`, `closed_irreversible`, `valid_u64_zero`, `find_map_update_other`, `find_map_update_same`

### sBPF Assembly

After `import SVM.SBPF` and `open SVM.SBPF` (from the qedsvm package):

**Types:** `Reg` (.r0 to .r10), `Src` (.reg/.imm), `Width` (.byte/.half/.word/.dword), `Insn` (all sBPF instructions), `Program` (Array Insn), `State` (regs, mem, pc, exitCode), `Mem` (Nat to Nat)

**Execution:** `executeFn` (function-based via match-based `progAt`, generated by `asm2lean`). `initState` (single pointer, r1=input), `initState2` (two pointers, r1=input, r2=insn data, with optional entryPc).

**Memory:** `readU8`, `readU16`, `readU32`, `readU64`, `writeU8` to `writeU64`, `effectiveAddr`

**Tactics:** `wp_exec [fetch_defs] [simp_extras]` is the one-shot sBPF proof tactic. `wp_step` for single-step manual control.

**Key lemmas:** `executeFn_halted`, `executeFn_step`, `executeFn_compose`, `readU64_writeU64_same`, `readU64_writeU64_disjoint`

## Proof Patterns

### Access control: signer must match authority

```lean
def cancelTransition (s : ProgramState) (signer : Pubkey) : Option Unit :=
  if signer = s.authority then some () else none

theorem cancel_access_control (s : ProgramState) (signer : Pubkey)
    (h : cancelTransition s signer ≠ none) :
    signer = s.authority := by
  unfold cancelTransition at h
  split_ifs at h with h_eq
  · exact h_eq
  · contradiction
```

### Conservation: invariant preserved across operations

```lean
def conservation (s : EngineState) : Prop := s.V >= s.C_tot + s.I

def depositTransition (s : EngineState) (amount : Nat) : Option EngineState :=
  if s.V + amount <= MAX_VAULT_TVL then
    some { V := s.V + amount, C_tot := s.C_tot + amount, I := s.I }
  else none

theorem deposit_conservation (s s' : EngineState) (amount : Nat)
    (h_inv : conservation s)
    (h : depositTransition s amount = some s') :
    conservation s' := by
  unfold depositTransition at h
  split_ifs at h with h_le
  · cases h
    unfold conservation at h_inv ⊢
    omega
  · contradiction
```

### State machine: lifecycle transitions

```lean
theorem cancel_closes_escrow (pre post : ProgramState)
    (h : cancelTransition pre = some post) :
    post.escrow.lifecycle = Lifecycle.closed := by
  unfold cancelTransition at h
  split_ifs at h with h_open
  cases h
  rfl
```

### CPI correctness: parameters match (pure rfl)

```lean
theorem cancel_cpi_correct (ctx : CancelContext) :
    let cpi := cancel_build_cpi ctx
    cpi.program = TOKEN_PROGRAM_ID ∧ cpi.amount = ctx.amount := by
  unfold cancel_build_cpi
  exact ⟨rfl, rfl⟩
```

## Critical Tactic Rules

| Do | Don't |
|---|---|
| `unfold f at h` before `split_ifs` | `simp [f] at h` before `split_ifs` (kills if-structure) |
| `unfold pred at h_inv ⊢` for named predicates | `unfold pred` only in goal (omega can't see hypotheses) |
| `cases h` after `split_ifs` on `some = some` | `injection h` (unnecessary) |
| `omega` for linear arithmetic | `norm_num` for linear goals |
| `exact ⟨rfl, rfl, rfl⟩` for conjunctions of rfl | `constructor` + `rfl` chains (verbose) |
| `simp [wrapAdd, toU64, ...] at h` to normalize hypotheses to match step-execution goals | `simp only [...]` for this (misses modular identities and numeric evaluation that step-level simp applied) |

## Common Errors and Fixes

| Error | Fix |
|---|---|
| `omega could not prove the goal` | Unfold named predicates in hypotheses: `unfold pred at h ⊢` |
| `no goals to be solved` | Remove redundant tactic (e.g., `· contradiction` after auto-closed branch) |
| `unknown constant 'X'` | Check imports; add `import QEDGen.Solana.X` or `open QEDGen.Solana` |
| `tactic 'split_ifs' failed, no if-then-else` | Use `unfold` first, not `simp` |
| `omega` fails on address disjointness after stack writes | Normalize hypotheses with `simp [wrapAdd, toU64, ...]` (not `simp only`) so address forms match the goal |

## Working Examples

### Escrow (Anchor)

A token escrow that lets two parties trade safely. Verified properties include access control on every handler, CPI correctness for token transfers, state-machine progress (`Open` to `Closed` is one-shot), and arithmetic safety on deposit. Spec lives at `examples/rust/escrow/escrow.qedspec`.

### Escrow-split (Anchor, multi-file)

The same escrow decomposed across `escrow.qedspec`, `handlers/initialize.qedspec`, `handlers/exchange.qedspec`, `handlers/cancel.qedspec`, and `properties.qedspec`, with the SPL Token interface imported from the bundled stdlib (`import Token from "spl"`) and pinned in `qed.toml` / `qed.lock`. Demonstrates spec composition across files and upstream interface dependencies.

### Multisig (Anchor)

M-of-N threshold signer gating with replay protection.

### Lending (Anchor)

Collateralized lending market with liquidation and interest accrual.

### Transfer (sBPF Assembly)

A native sBPF lamport transfer program. Verified properties: input validation, duplicate account rejection, balance sufficiency.

### Slippage (sBPF Assembly)

A SIMD-0321-style slippage guard.

## Environment Variables

- `MISTRAL_API_KEY`: required only for `fill-sorry` and `generate` (Leanstral sorry-filling). Free from console.mistral.ai.
- `ARISTOTLE_API_KEY`: required only for `aristotle` commands. Get at aristotle.harmonic.fun.
- `QEDGEN_VALIDATION_WORKSPACE`: optional override for the global Mathlib cache location.

## Requirements

- Rust toolchain — user-managed, needed for source builds and generated Rust tests
- Lean 4 / elan — user-managed, needed for formal proofs
- Kani — user-managed, needed for Kani verification
- Git (QEDGen is git-native: spec changes and regeneration are safe to merge)
- `MISTRAL_API_KEY` only when calling `fill-sorry` or `generate`
- `ARISTOTLE_API_KEY` only when calling `aristotle`

Spec writing, `check`, `codegen`, and `verify` require no API keys.

## License

MIT