my-project-public

repository

loading code, commits, and activity

repositories

loading repo index

#1	<p align="center">
#2	<picture>
#3	<source media="(prefers-color-scheme: dark)" srcset="docs/logo-dark.png">
#4	<source media="(prefers-color-scheme: light)" srcset="docs/logo-light.png">
#5	<img src="docs/logo-dark.png" alt="QEDGen" width="260">
#6	</picture>
#7	</p>
#8
#9	<h3 align="center">Prove your Solana code is correct. Mathematically.</h3>
#10
#11	<p align="center">
#12	<a href="https://qedgen.dev">Website</a> ·
#13	<a href="https://github.com/qedgen/solana-skills/blob/main/SKILL.md">Docs</a> ·
#14	<a href="https://github.com/qedgen/solana-skills/issues">Issues</a>
#15	</p>
#16
#17	<p align="center">
#18	<a href="https://github.com/qedgen/solana-skills/blob/main/LICENSE"><img src="https://img.shields.io/badge/license-MIT-blue.svg" alt="MIT License"></a>
#19	<a href="https://qedgen.dev"><img src="https://img.shields.io/badge/site-qedgen.dev-38bdf8" alt="Website"></a>
#20	</p>
#21
#22	---
#23
#24	An agent skill that formally verifies Solana programs by generating Lean 4 proofs. Your agent writes the proofs; Mistral's Leanstral model handles hard sub-goals.
#25
#26	```bash
#27	npx skills add qedgen/solana-skills
#28	```
#29
#30	> Works with Claude Code, Cursor, Windsurf, GitHub Copilot, and any agent supporting the [Agent Skills](https://agentskills.io) spec.
#31
#32	## How it works
#33
#34	```
#35	Your Code ──► Your Agent ──► SPEC.md ──► Lean 4 Proofs ──► lake build ──► ∎
#36	│ ▲
#37	│ │
#38	└─── iterate on errors ─────┘
#39	Leanstral fills
#40	hard sub-goals
#41	```
#42
#43	1. Your agent reads the program source and IDL
#44	2. Generates a `SPEC.md` with verification goals and properties
#45	3. Writes Lean 4 proofs against the QEDGen support library
#46	4. Iterates on `lake build` errors until proofs compile
#47	5. Calls `qedgen fill-sorry` for hard sub-goals (powered by Leanstral)
#48
#49	## What it verifies
#50
#51	\| Property \| Approach \|
#52	\|---\|---\|
#53	\| Access control \| Signer checks, authority constraints \|
#54	\| CPI correctness \| Correct parameters passed to each transfer (axiomatic, pure `rfl`) \|
#55	\| State machines \| Lifecycle correctness, one-shot safety \|
#56	\| Arithmetic safety \| Overflow/underflow for fixed-width integers \|
#57
#58	CPI calls are axiomatic — we verify the program passes correct parameters. SPL Token internals and the Solana runtime are trusted.
#59
#60	## Setup
#61
#62	Export a [Mistral API key](https://console.mistral.ai) (free tier available):
#63
#64	```bash
#65	export MISTRAL_API_KEY=your_key_here
#66	```
#67
#68	The installer handles Rust, Lean/elan, the CLI binary, and global Mathlib cache automatically. First Mathlib build takes 15-45 min; subsequent builds reuse the cache.
#69
#70	## Usage
#71
#72	### Full pipeline
#73
#74	```bash
#75	qedgen verify \
#76	--idl target/idl/my_program.json \
#77	--validate
#78	```
#79
#80	### Generate from an existing prompt
#81
#82	```bash
#83	qedgen generate \
#84	--prompt-file /tmp/analysis/property.prompt.txt \
#85	--output-dir /tmp/proof \
#86	--passes 4 \
#87	--validate
#88	```
#89
#90	### Fill hard sub-goals
#91
#92	```bash
#93	qedgen fill-sorry \
#94	--file formal_verification/Proofs/Hard.lean \
#95	--passes 3 \
#96	--validate
#97	```
#98
#99	### Consolidate proofs
#100
#101	```bash
#102	qedgen consolidate \
#103	--input-dir /tmp/proofs \
#104	--output-dir my_program/formal_verification
#105	```
#106
#107	## Examples
#108
#109	- [Escrow](example/escrow/) — Token escrow with authority checks, CPI transfer verification, and lifecycle proofs
#110	- [Percolator](example/percolator/) — Market maker with state machine verification and arithmetic safety
#111
#112	## Requirements
#113
#114	- `MISTRAL_API_KEY` environment variable
#115	- Rust toolchain (auto-installed if missing)
#116	- Lean 4 / elan (auto-installed if missing)
#117
#118	Override the Mathlib cache location with `QEDGEN_VALIDATION_WORKSPACE`.
#119
#120	## License
#121
#122	[MIT](LICENSE)
#123

z6Mkq5mY3JWtxoxUobWcfNHm7AkRubgSWEZTkBVqZXJviFZ5/my-project-public