Where proof is the difference

Testing samples behaviour; verification proves it. Where a wrong answer is irreversible — money moved, inventory lost, a payment captured twice — the difference between "it worked in the tests" and "it holds for every valid state" is the difference between a bug report and a liability.

Money movement

Transfers that conserve funds, forbid overdrafts, and keep every balance non-negative — stated as predicates over the whole state space, not a table of examples.

Conservation — total balance is unchanged by every transfer.
No overdraft — every balance stays non-negative, before and after.
Frame discipline — the contract declares exactly what it reads and writes.

Exactly-once fulfilment

Orders that reserve inventory, capture payment, and emit events atomically — and idempotently, so a retried worker cannot double-charge.

Exactly-once — at most one worker observes success for a given order.
No lost inventory — a failed reservation consumes nothing.
Composable proof — the top-level guarantee is proved from sub-contracts.

Inventory & reservations

Reservation logic where failure leaves the system exactly as it was — safe retries by construction, not by convention.

Rollback on failure — no partial state on a failed reserve.
Safe retry — a failed attempt is provably invisible to the caller.

Regulatory compliance

Rules your system must never violate, stated as invariants the prover checks against every execution path — not as a checklist you hope the code obeys.