An agent skill that verifies your core business logic. Your agent reads the code, writes Lean 4 proofs, and iterates until they compile. Hard sub-goals go to Leanstral, Mistral's theorem prover.
npx skills add qedgen/solana-skillsWorks with Cursor, Windsurf, Claude Code, GitHub Copilot, and any agent supporting Agent Skills.
Your agent drives proof writing directly. Full code context, no lossy pipeline.
Agent reads your Rust / Anchor source, existing specs, or IDLs.
Generates security goals, state model, and formal properties from your code.
Writes theorems, runs lake build, iterates until everything compiles.
Hard sub-goals go to Leanstral. Every theorem compiles or it doesn't ship.
16 verified proofs across two programs. Every proof compiles via lake build.
Token escrow for two-party trades. Initializer deposits, taker completes, or initializer cancels.
-- Cancel only succeeds if signer = initializer
theorem cancel_access_control
(p_preState : ProgramState) (p_signer : Pubkey)
(h : cancelTransition p_preState p_signer ≠ none) :
p_signer = p_preState.escrow.initializer := by
unfold cancelTransition at h
split_ifs at h with h_eq
· exact h_eq
· contradictionPerpetual DEX risk engine with protected principal and lazy side indices. Non-Anchor, no_std.
-- Deposit preserves V >= C_tot + I
theorem deposit_conservation
(p_s p_s' : EngineState) (p_amount : Nat)
(h_inv : conservation p_s)
(h : depositTransition p_s p_amount = some p_s') :
conservation p_s' := by
unfold depositTransition at h
split_ifs at h with h_le
cases h
unfold conservation at h_inv ⊢
dsimp only
omeganpx skills add qedgen/solana-skillsFormally verify this program.