qedgen（qedgen 搜索）

QEDGen

Trigger And Mission

Use this skill when the user wants to verify Solana program behavior, write or review a .qedspec, generate verification artifacts, onboard an existing Anchor program, or keep generated artifacts in sync.

Mission:

• Read the source before writing the spec.
• Treat .qedspec as the single source of truth.
• Use qedgen check to validate the spec.
• Use qedgen codegen to scaffold generated artifacts.
• Fill generated Rust handler TODOs as an agent task, then build and test.
• Use qedgen verify and drift gates to keep proofs and code synchronized.

Do not present generated Rust as complete business logic. Anchor and Quasar output is an implementation scaffold. Handler files can intentionally contain todo!() for transfers, events, CPI wiring, and non-mechanical effects until the agent fills them.

How To Run QEDGen

Prefer the installed skill wrapper when available:

QEDGEN="$HOME/.agents/skills/qedgen/tools/qedgen"

From a repo checkout, the local binary also works:

cargo run -p qedgen-solana-skills -- <command>

Every write path expects a git repo. If the command errors outside a repo, run git init or move into the project root.

Common commands:

$QEDGEN check --spec program.qedspec
$QEDGEN codegen --spec program.qedspec --all
$QEDGEN verify --spec program.qedspec
$QEDGEN reconcile --spec program.qedspec --code programs/ --proofs formal_verification/

Release and repo-maintenance gates:

bash scripts/check-version-consistency.sh
bash scripts/check-readme-drift.sh
$QEDGEN check --regen-drift

Read references/cli.md for the full CLI surface and flags.

Flow: Validate -> Scaffold -> Fill -> Verify

Step 1. Understand the program.

Read the Rust source, tests, account model, authorities, PDAs, token flows, arithmetic, and lifecycle. For a returning QEDGen project, read the .qedspec next to the code. Do not treat Spec.lean as source; it is generated.

Step 2. Validate the spec.

$QEDGEN check --spec program.qedspec --coverage
$QEDGEN check --spec program.qedspec --json

Fix lint, coverage, import, lifecycle, arithmetic, and CPI-shape findings in the .qedspec first. The spec should describe the intended behavior before codegen or proof work begins.

Step 3. Scaffold generated artifacts.

$QEDGEN codegen --spec program.qedspec --target anchor --all

Use --target quasar for Quasar. Pinocchio is reserved and should not be promised as complete.

Step 4. Fill generated Rust.

Open generated handler files that contain todo!(). Fill business logic using the guard calls, state structs, and spec effects as the contract. Then run the framework build and tests until compile-clean:

cargo check --manifest-path programs/Cargo.toml
cargo test --manifest-path programs/Cargo.toml

Step 5. Verify generated backends.

$QEDGEN verify --spec program.qedspec --proptest
$QEDGEN verify --spec program.qedspec --kani
$QEDGEN verify --spec program.qedspec --lean

Run only the backends relevant to artifacts present in the project. For generated examples in this repo, also run:

$QEDGEN check --regen-drift

Brownfield Onboarding

For an existing Anchor program:

$QEDGEN adapt --program programs/my_program --out program.qedspec

Then fill TODOs in the .qedspec, validate it, and cross-check against the live program:

$QEDGEN check --spec program.qedspec --anchor-project programs/my_program

After the spec covers each handler, stamp source drift attributes:

$QEDGEN adapt --program programs/my_program --spec program.qedspec

Paste the emitted #[qed(verified,...)] attributes above the matching handler functions. Future handler-body, accounts-constraint, or spec edits should fail the build until the attributes are intentionally refreshed.

If handler dispatch is non-standard, use explicit overrides:

$QEDGEN adapt --program programs/my_program --handler deposit=processor::deposit

For IDL-only onboarding:

$QEDGEN spec --idl target/idl/my_program.json

IDL scaffolds are shape-only. They need source review before they can express semantic guarantees.

Codegen Ownership

Generated and always safe to regenerate:

User-owned after first scaffold:

Generated support code should compile around intentional handler TODOs. If support code fails to compile, fix the generator or generated support. If handler business logic is missing, fill the handler.

Proof Handoff

Use proof engineering only when tests and bounded model checking are insufficient.

Use proptest for:

• Fast counterexamples during spec iteration.
• Randomized state transitions.
• Cheap regression checks.

Use Kani for:

• Access control.
• Arithmetic safety.
• Conservation and isolation invariants.
• Bounded state-machine properties.

Use Lean for:

• DeFi math that needs symbolic reasoning beyond bounded search.
• Wide arithmetic solvency arguments.
• Inductive sBPF bytecode proofs.
• Proof obligations where Kani/proptest cannot give enough confidence.

Use Leanstral for routine sorry filling and Aristotle for harder long-running proof search. Read references/proof-patterns.md before proof repair and references/sbpf.md for sBPF.

Always run lake build after editing Lean and run qedgen check after proofs compile so orphan or missing obligations are reported.

References

Load references on demand. Do not bulk-load all files.