Governor Form
The Governor form defines on-chain governance with six state fields — proposals (Nat), votes_for and votes_against (Nat per proposal ID), voted (Bool per Address per proposal ID), quorum (Nat), and phase (Phase per proposal ID) — and proves two invariants at compile time: quorum enforcement requiring votes_for[id] >= quorum before any proposal executes, and double-vote prevention ensuring no address votes twice on the same proposal. The compiler verifies quorum by structural analysis of the execute transition's require guard, and double-vote prevention by proving the voted mapping is a monotonic flag checked before every vote mutation. Both proven invariants are erased from WASM output, producing zero-overhead verified governance contracts deployable to CosmWasm, Near, Stylus, and Polkadot.
form Governor { state { proposals : Nat votes_for : Nat per Nat votes_against : Nat per Nat voted : Bool per Address per Nat quorum : Nat phase : Phase per Nat } invariant quorum_required : execute(id) => votes_for[id] >= quorum invariant no_double_vote : vote(id, sender) => !voted[sender][id] transition propose() { proposals += 1 phase[proposals] = Phase.Voting votes_for[proposals] = 0 votes_against[proposals] = 0 } -- initializes a new proposal in Voting phase with zero tallies transition vote(id, support) { require phase[id] == Phase.Voting require !voted[msg.sender][id] voted[msg.sender][id] = true if support then votes_for[id] += 1 else votes_against[id] += 1 } -- no_double_vote: require !voted guard + monotonic flag set transition execute(id) { require phase[id] == Phase.Voting require votes_for[id] >= quorum phase[id] = Phase.Executed } -- quorum_required: require guard enforces threshold before execution }
State Fields
proposals : Nat — counter tracking the total number of proposals created. Each new proposal increments this counter and uses it as its ID.
votes_for : Nat per Nat — maps each proposal ID to its count of supporting votes.
votes_against : Nat per Nat — maps each proposal ID to its count of opposing votes.
voted : Bool per Address per Nat — double-indexed mapping tracking whether a given address has voted on a given proposal. Monotonic: once true, never reset.
quorum : Nat — the minimum number of supporting votes required to execute a proposal.
phase : Phase per Nat — maps each proposal ID to its lifecycle phase (Voting or Executed).
Invariant: Quorum Required
The quorum invariant execute(id) => votes_for[id] >= quorum asserts that proposal execution requires sufficient support. The compiler proves this by analyzing the execute transition:
The execute transition contains require votes_for[id] >= quorum as a precondition before phase[id] = Phase.Executed. The compiler verifies that every control-flow path reaching the phase mutation passes through this guard. Since the require statement is the sole gateway, the quorum threshold is structurally enforced — not by convention, but by the algebraic structure of the transition.
Invariant: No Double Vote
The double-vote invariant vote(id, sender) => !voted[sender][id] asserts that no address can cast more than one vote per proposal. The compiler proves this through monotonicity analysis:
The vote transition checks require !voted[msg.sender][id] before setting voted[msg.sender][id] = true. The compiler verifies three properties: (1) the require guard rejects calls where voted is already true, (2) voted is set to true within the same atomic transition, (3) no transition anywhere in the form resets voted to false. This makes voted a monotonic flag — once set, permanently set — and double voting is algebraically excluded from all reachable states.
Transitions
propose() — creates a new proposal. Increments the proposals counter, initializes the phase to Voting, and zeroes the vote tallies. No authorization required — any address can propose.
vote(id, support) — casts a vote on a proposal. Requires the proposal is in Voting phase and the sender has not already voted. The voted flag is set monotonically, preventing any future vote on the same proposal from the same address.
execute(id) — executes a proposal that has reached quorum. Requires the proposal is in Voting phase and votes_for meets the quorum threshold. Transitions the proposal to the Executed phase.
Frequently Asked Questions
- What invariants does a Governor form prove?
- The Governor form proves two invariants: quorum enforcement (proposals only execute when votes_for >= quorum) and double-vote prevention (no address votes twice on the same proposal). Both are verified at compile time by analyzing the algebraic structure of transitions — the compiler proves that every path to execution passes through the quorum guard, and that the voted mapping is monotonic, making duplicate votes structurally impossible.
- How does Formagine verify quorum enforcement?
- The compiler analyzes the execute transition and identifies the require votes_for[id] >= quorum guard as the sole precondition before the phase mutation. It then proves that no control-flow path can reach phase[id] = Phase.Executed without satisfying this guard. The proof is structural: it depends on the transition's control flow graph, not on specific runtime values. This means quorum enforcement holds for all possible vote counts and all possible execution sequences.
- How does the Governor form prevent double voting?
- The vote transition checks require !voted[msg.sender][id] then sets voted[msg.sender][id] = true. The compiler proves monotonicity: voted starts false, is set to true exactly once per (address, proposal) pair, and no transition resets it. A second vote attempt from the same address hits the require !voted guard and is rejected. This is not a runtime check that could be bypassed — it is an algebraic property of the state machine that the compiler proves holds for all reachable states.
- What chains can the Governor form compile to?
- The Governor form compiles to optimized WASM targeting CosmWasm (Cosmos ecosystem), Near Protocol, Arbitrum Stylus (Ethereum L2), and Polkadot (ink! contracts). The same form definition produces verified governance contracts for all targets with identical quorum and double-vote guarantees.