repositories
loading repo index
repositories
loading repo index
repository
loading code, commits, and activity
public Clawd ADK gateway launch mirror
stars
latest
clone command
git clone gitlawb://did:key:z6Mkq5mY...iFZ5/my-project-publ...git clone gitlawb://did:key:z6Mkq5mY.../my-project-publ...2fa351d6docs: add automaton and perps launch sources16d ago| #1 | # QEDGen |
| #2 | |
| #3 | > 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. Install with `npx skills add qedgen/solana-skills`. Works with any coding agent supporting the Agent Skills spec. |
| #4 | |
| #5 | QEDGen verifies your core business logic. Your agent reads the codebase, writes Lean 4 models and proofs, iterates on compiler errors, and calls Leanstral (Mistral's theorem prover) only for hard sub-goals. |
| #6 | |
| #7 | ## Docs |
| #8 | |
| #9 | - [README](https://raw.githubusercontent.com/qedgen/solana-skills/main/README.md): Installation, usage, CLI commands, and requirements |
| #10 | - [SKILL.md](https://raw.githubusercontent.com/qedgen/solana-skills/main/SKILL.md): Full proof-writing workflow, support library API, proof patterns, tactic rules, and error fixes |
| #11 | - [CLAUDE.md](https://raw.githubusercontent.com/qedgen/solana-skills/main/CLAUDE.md): Build commands, architecture, crate structure, and development guide |
| #12 | |
| #13 | ## Examples |
| #14 | |
| #15 | - [Escrow Proofs](https://raw.githubusercontent.com/qedgen/solana-skills/main/example/escrow/formal_verification/EscrowProofs.lean): 9/9 verified proofs for an Anchor token escrow (access control, state machines, arithmetic safety) |
| #16 | - [Escrow Spec](https://raw.githubusercontent.com/qedgen/solana-skills/main/example/escrow/formal_verification/SPEC.md): Verification spec for the escrow program |
| #17 | - [Percolator Proofs](https://raw.githubusercontent.com/qedgen/solana-skills/main/example/percolator/formal_verification/PercolatorProofs.lean): 7/7 verified proofs for a pure Rust risk engine (conservation, arithmetic safety, state machine, fee isolation) |
| #18 | - [Percolator Spec](https://raw.githubusercontent.com/qedgen/solana-skills/main/example/percolator/formal_verification/SPEC.md): Verification spec for the percolator engine |
| #19 | |
| #20 | ## Optional |
| #21 | |
| #22 | - [Verification Scope](https://raw.githubusercontent.com/qedgen/solana-skills/main/example/escrow/formal_verification/VERIFICATION_SCOPE.md): What is verified vs. trusted as axioms |
| #23 | - [Lean Support Library](https://raw.githubusercontent.com/qedgen/solana-skills/main/crates/qedgen/lean_support/QEDGen.lean): Root import for the Solana axiom library |
| #24 |