my-project-public

repository

loading code, commits, and activity

repositories

loading repo index

#1	# CLAUDE.md
#2
#3	This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.
#4
#5	## Overview
#6
#7	QEDGen is a Claude Code skill for formally verifying Solana programs using Lean 4 proofs. Claude (the local LLM) drives proof writing directly — reading code, writing Lean models/theorems/proofs, and iterating on `lake build` errors. Leanstral (Mistral's theorem prover) is called only for hard sub-goals via `fill-sorry`.
#8
#9	Core workflow: Claude reads source → writes SPEC.md → writes Lean 4 proofs → `lake build` → iterates → calls `qedgen fill-sorry` for hard sub-goals
#10
#11	## Build and Development Commands
#12
#13	### Build the CLI
#14
#15	```bash
#16	# Build qedgen binary (outputs to ./bin/qedgen)
#17	cargo build --release
#18
#19	# Build just the Lean support library
#20	cd crates/qedgen/lean_support
#21	lake build
#22	```
#23
#24	### Run Tests
#25
#26	```bash
#27	# Rust unit tests
#28	cargo test
#29
#30	# Test Lean support library axioms
#31	cd crates/qedgen/lean_support
#32	lake env lean test_lemmas.lean
#33
#34	# Build the example escrow verification
#35	cd example/escrow/formal_verification
#36	lake build # Verify all proofs compile
#37	```
#38
#39	### QEDGen Commands
#40
#41	```bash
#42	# Set up global validation workspace (first time: 15-45 min for Mathlib)
#43	qedgen setup
#44
#45	# Generate proofs from a prompt file (used by Claude internally)
#46	qedgen generate \
#47	--prompt-file /tmp/proof/prompt.txt \
#48	--output-dir /tmp/proof \
#49	--passes 3 \
#50	--temperature 0.3 \
#51	--validate
#52
#53	# Fill sorry markers in a Lean file (Claude calls this for hard sub-goals)
#54	qedgen fill-sorry \
#55	--file formal_verification/Proofs/Hard.lean \
#56	--passes 3 \
#57	--validate
#58
#59	# Generate a draft SPEC.md from an Anchor IDL
#60	qedgen spec --idl target/idl/program.json --output-dir ./formal_verification
#61
#62	# Consolidate multiple proof projects into single project
#63	qedgen consolidate \
#64	--input-dir /tmp/proofs \
#65	--output-dir formal_verification
#66	```
#67
#68	## Architecture
#69
#70	### Crate Structure
#71
#72	`crates/qedgen/` - Single crate: CLI and Mistral API client
#73	- `main.rs` - CLI entry points (generate, fill-sorry, spec, consolidate, setup)
#74	- `api.rs` - Mistral API client, pass@N sampling, sorry-filling, retry logic
#75	- `validate.rs` - Lake build validation in persistent workspace
#76	- `project.rs` - Lean project scaffolding generation
#77	- `consolidate.rs` - Merges multiple proof projects
#78	- `spec.rs` - SPEC.md generation from Anchor IDL
#79
#80	`crates/qedgen/lean_support/` - Canonical Lean axioms for Solana
#81	- `QEDGen/Solana/Account.lean` - Account structure
#82	- `QEDGen/Solana/Token.lean` - Token operations and conservation axioms
#83	- `QEDGen/Solana/Authority.lean` - Authorization predicates
#84	- `QEDGen/Solana/State.lean` - Lifecycle and state machines
#85
#86	### Key Design Decisions
#87
#88	Why Claude-driven (not pipeline-driven)?
#89	- Claude reads code context and writes proofs directly — no lossy analyzer step
#90	- Proof patterns generalize across programs without per-property prompt templates
#91	- Claude iterates on `lake build` errors naturally
#92	- Scales to large programs without combinatorial prompt explosion
#93
#94	Why Leanstral model only for sorry-filling?
#95	- Full module generation requires too much context (import ordering, namespace management)
#96	- Focused sorry-filling gives Leanstral maximum signal with minimal noise
#97	- Claude handles the modeling/structuring; Leanstral handles hard tactic proofs
#98
#99	Why pass@N sampling?
#100	- The Leanstral model is non-deterministic; multiple attempts increase success rate
#101	- Validation selects compilable proof over heuristics (sorry count)
#102
#103	Why persistent validation workspace?
#104	- Lake's first Mathlib build takes 15-45 minutes
#105	- Reusing `.lake/packages/` avoids repeated Mathlib compilation
#106	- Location: platform cache dir or `QEDGEN_VALIDATION_WORKSPACE`
#107
#108	Why axioms instead of proving SPL Token?
#109	- Verification scope: program logic only (see VERIFICATION_SCOPE.md)
#110	- Trust boundary: SPL Token, Solana runtime, CPI mechanics
#111	- Pragmatic: keeps proofs tractable and completion time reasonable
#112
#113	## Verification Scope
#114
#115	What we verify:
#116	- Authorization (signer checks, constraints)
#117	- Conservation (token totals preserved)
#118	- State machines (lifecycle, one-shot safety)
#119	- Arithmetic safety (overflow/underflow)
#120	- CPI correctness (parameters match intent)
#121
#122	What we trust (axioms):
#123	- SPL Token implementation
#124	- Solana runtime (PDA derivation, account ownership)
#125	- CPI mechanics
#126	- Anchor framework
#127
#128	See `example/escrow/formal_verification/VERIFICATION_SCOPE.md` for details.
#129
#130	## Common Development Tasks
#131
#132	### Adding New Axioms
#133
#134	When a proof pattern is reusable across programs:
#135
#136	1. Add to `crates/qedgen/lean_support/QEDGen/Solana/Token.lean` (or other module)
#137	2. Document the trust assumption with a comment
#138	3. Export in `QEDGen.lean`
#139	4. Update SKILL.md support library API section
#140	5. Test: `cd crates/qedgen/lean_support && lake build`
#141
#142	### Debugging Failed Proofs
#143
#144	If `lake build` fails:
#145	1. Read the error output directly
#146	2. Common issues:
#147	- `split_ifs` fails → use `unfold` before `split_ifs`
#148	- `omega could not prove` → unfold named predicates in BOTH hypothesis and goal: `unfold pred at h ⊢`
#149	- `no goals to be solved` → remove redundant tactic (e.g., `· contradiction` after auto-closed branch)
#150	- `unexpected token 'open'` → use `«open»` quoting for Lean keywords
#151	- Namespace collision → check `open` statements
#152	3. Fix the proof and re-run `lake build`
#153
#154	## Environment Variables
#155
#156	- `MISTRAL_API_KEY` - Required for `fill-sorry` and `generate` commands
#157	- `QEDGEN_VALIDATION_WORKSPACE` - Override validation workspace path (default: platform cache dir)
#158
#159	## Common Lean Proof Patterns
#160
#161	### Tactic Sequencing
#162	```lean
#163	-- BAD: simp eliminates if-structure
#164	simp [transition] at h
#165	split_ifs at h -- ERROR
#166
#167	-- GOOD: unfold preserves structure
#168	unfold transition at h
#169	split_ifs at h with h_eq
#170	```
#171
#172	### Conservation Proofs
#173	```lean
#174	-- CRITICAL: unfold named predicate in BOTH hypothesis and goal
#175	unfold conservation at h_inv ⊢
#176	omega
#177	```
#178
#179	### CPI Correctness (pure rfl)
#180	```lean
#181	theorem cpi_correct (ctx : Context) :
#182	let cpi := build_cpi ctx
#183	cpi.program = TOKEN_PROGRAM_ID ∧ cpi.amount = ctx.amount := by
#184	unfold build_cpi
#185	exact ⟨rfl, rfl⟩
#186	```
#187
#188	## Output Artifacts
#189
#190	After `qedgen generate`:
#191	```
#192	/tmp/proof/
#193	├── Best.lean # Selected best completion
#194	├── metadata.json # Rankings, timings, tokens
#195	├── prompt.txt # Prompt sent to Leanstral model
#196	├── attempts/
#197	│ ├── completion_0.lean
#198	│ ├── completion_0_raw.txt
#199	│ └── ...
#200	└── validation/
#201	└── completion_0.log # Lake build log
#202	```
#203
#204	## Notes
#205
#206	- First Lean build is expensive (15-45 min for Mathlib). Run `qedgen setup` first.
#207	- If `lake build` fails with "could not resolve 'HEAD' to a commit", remove `.lake/packages/mathlib` and run `lake update`.
#208	- Binary is built to `./bin/qedgen`, not `target/release/qedgen`.
#209	- The SKILL.md file defines the full proof-writing workflow that Claude follows.
#210

z6Mkq5mY3JWtxoxUobWcfNHm7AkRubgSWEZTkBVqZXJviFZ5/my-project-public