qedgen

QEDGen — Agent-Driven Formal Verification

You (Claude) are the proof engineer. You read the codebase, write Lean 4 models and proofs, iterate on compiler errors, and call Leanstral (Mistral's theorem prover) only for hard sub-goals you cannot fill yourself.

Architecture

You (Claude)                          Leanstral (remote model)
  ├── Read spec / source code           ├── Fill sorry markers
  ├── Write Lean 4 models               └── Suggest tactics for hard goals
  ├── Write theorem statements
  ├── Write proof attempts
  ├── Run `lake build`, read errors
  └── Fix and iterate

Step 1: Understand the program

Check for existing artifacts in this priority order:

1. spec.md exists → Read it. An existing spec captures the author's intent, state model, invariants, and operations. Extract security goals, state model, and formal properties. Skip the scoping quiz and go directly to Step 2.
2. IDL exists (target/idl/<program>.json) → Run qedgen spec --idl <path> to generate a draft SPEC.md with TODO markers, then refine interactively.
3. Neither exists → Read the source code directly. Ask broader scoping questions.

Step 2: Scope the verification

If no spec.md was found, run a short interactive quiz — one question at a time, with checkbox options derived from the program's structure. Ask about functionality and risks, not implementation details.

Question 1: "What does this program need to guarantee above all else?" Options derived from the program's structure:

• Authorization / access control
• Tokens are never lost / correct routing
• One-shot safety / no replay
• Arithmetic safety / no overflow
• Conservation (e.g., vault >= total claims)
• All of the above

Question 2: "Which scenario worries you most?" Generate concrete risk scenarios from the program.

Question 3: "Does the program make any assumptions that aren't enforced on-chain?"

Ask questions one at a time. Wait for the user's answer before presenting the next question.