Form Templates
Each form is an algebraic type with embedded invariants proven at compile time. Select a template to see its state fields, invariants, transitions, and the algebraic verification strategy the compiler uses. All forms compile to optimized WASM targeting CosmWasm, Near, Stylus, and Polkadot.
Token
invariant conservation : sum(balance) == supply
Fungible token with algebraic supply conservation. The compiler proves that transfer, mint, and burn all preserve the identity sum(balance) == supply by extracting arithmetic cancellations and co-variance relationships. No tokens can be created or destroyed outside authorized paths.
transfer · mint · burn
Vault
invariant conservation : sum(deposited) == total
invariant time_lock : withdraw => block.time >= lock_until
invariant time_lock : withdraw => block.time >= lock_until
Asset vault with deposit conservation and time-lock enforcement. The compiler proves that deposit and withdraw preserve sum(deposited) == total by co-variance, and that withdrawal paths are gated by the block.time >= lock_until precondition.
deposit · withdraw
Escrow
invariant single_release : released => amount == 0
Multi-party escrow with single-release guarantee. The compiler proves that once funds are disbursed (to beneficiary or refunded to depositor), the escrowed amount is zero and no further extraction is possible. Arbiter-only release and deadline-gated refunds verified by structural control-flow analysis.
release · refund
Governor
invariant quorum_required : execute(id) => votes_for[id] >= quorum
invariant no_double_vote : vote(id, sender) => !voted[sender][id]
invariant no_double_vote : vote(id, sender) => !voted[sender][id]
On-chain governance with quorum enforcement and double-vote prevention. The compiler proves that proposal execution requires sufficient votes and that the voted mapping is a monotonic flag — once set, never reset — making duplicate votes algebraically impossible.
propose · vote · execute
Marketplace
invariant fee_cap : fee_rate <= 1000
Decentralized marketplace with fee cap enforcement. The compiler performs bounds analysis to prove fee_rate never exceeds 1000 (10%), then derives that the fee calculation fee = price * fee_rate / 10000 is bounded by price / 10 for every purchase. Buyers and sellers are protected from excessive fees by construction.
list · buy