proofs, not promises
Ship without fear
Describe what your Solana program must guarantee in .qedspec.
QEDGen finds the bugs your tests miss, then generates the proofs, property tests,
and CI to keep them fixed.
Works with Claude Code, Codex, Cursor, Windsurf, and any agent supporting Agent Skills.
escrow.qedspec
SPEC
// Token escrow: two parties trade safely.spec Escrow type State | Uninitialized | Open of { initializer_amount : U64, taker_amount : U64 } | Closed handler initialize (deposit : U64) : State.Uninitialized -> State.Open { auth initializer requires deposit > 0 else InvalidAmount transfers { from initializer_ta to escrow_ta amount deposit } emits EscrowInitialized}
generates
tests/proptest.rs
proptest
formal_verification/Proofs.lean
Lean 4
tests/kani.rs
Kani · SMT
.github/workflows/verify.yml
CI