executable protocol specs in Python you can verify

wunderspec

a protocol specification framework for:

  • - senior systems engineers
  • - security researchers
  • - systems architects
  1. [01]specify in Python with strong formal grounds
  2. [02]linter, executor, checker, translator
  3. [03]easy for humans and LLMs to read and write
request access

or request a demo at

payment.py 
from wunderspec import *

@action
def process_charge(c: Context[PaymentState]):
    s = c.state
    c.assume(~s.command_queue.is_empty)
    cmd = s.command_queue[0]
    c.assume(cmd.kind == CHARGE_COMMAND)
    c.assume(command_ok(s, cmd))
    c.assume(s.payment[cmd.txn].status == NEW)
    c.assume(event_count(s, cmd.txn, CHARGED) == 0)
    c.assume(s.balance[cmd.payer] >= cmd.amount)

    s.event_queue += List(payment_event(CHARGED, cmd.txn))
    s.balance[cmd.payer] -= cmd.amount
    s.balance[cmd.merchant] += cmd.amount
    s.payment[cmd.txn] = payment_details(cmd, CHARGED)
    s.ledger[cmd.txn] += List(CHARGED)
    s.command_queue = s.command_queue[1:]


@invariant
def no_overdraft(s: PaymentState) -> BoolExpr:
    return Forall(s.balance[account] >= 0 for account in accounts(s))


@invariant
def no_double_charge(s: PaymentState) -> BoolExpr:
    return Forall(event_count(s, txn, CHARGED) <= Val(1) for txn in s.Txn)

$ wunderspec check --property=all_inv payment.py

[ok] no_overdraft

[ok] no_double_charge