Stock exchange

Available in the dashboard. Run speclogician demo run stock-exchange to load this spec, then open it via speclogician demo dashboard stock-exchange or the VS Code extension (status-bar SpecLogician / Browser button).

This example formalizes a tiny single-security order book — at most one resting bid and one resting ask — with cancels and a safety invariant: the book must never become crossed (best_bid >= best_ask). It's the cleanest demo in the repo for showing how is_bad scenarios drive safety analysis.

The system

A single security with one resting bid and one resting ask at a time. 0 means "no order on that side."
Incoming orders are buys, sells, or a cancel-all.
A buy at p >= best_ask lifts the ask and prints at the ask's price.
A sell at p <= best_bid hits the bid and prints at the bid's price.
Otherwise, the order rests if it improves the same-side top of book.
Invariant: the book must never be locked (best_bid > 0 ∧ best_ask > 0 ∧ best_bid >= best_ask).

Domain base

type state = {
  best_bid   : int;
  best_ask   : int;
  last_price : int;
  num_trades : int;
}
 
type action = {
  side  : int;   (* 0 = cancel-all, 1 = buy, 2 = sell *)
  price : int;
  qty   : int;
}

Design notes:

best_bid / best_ask use 0 as a sentinel meaning "no order on that side". Production exchanges typically use Option int here; the integer encoding keeps the demo small.
num_trades counts executed trades — used by the has_traded predicate to label post-trade observation states.
The action's side is an int (0/1/2) for compactness; in a fuller spec you'd use a variant type to eliminate meaningless side = 5 complement regions.

Predicates

State predicates

Name	IML body	Meaning
`book_empty`	`s.best_bid = 0 && s.best_ask = 0`	No resting orders on either side
`bid_only`	`s.best_bid > 0 && s.best_ask = 0`	Only a resting bid
`ask_only`	`s.best_bid = 0 && s.best_ask > 0`	Only a resting ask
`book_locked`	`s.best_bid > 0 && s.best_ask > 0 && s.best_bid >= s.best_ask`	Crossed/locked — this is the bad state
`no_trades_yet`	`s.num_trades <= 0`	No trades have executed yet
`has_traded`	`s.num_trades > 0`	At least one trade has executed

Action predicates

Name	IML body	Meaning
`is_buy`	`a.side = 1`	Incoming buy
`is_sell`	`a.side = 2`	Incoming sell
`is_cancel`	`a.side = 0`	Cancel-all
`valid_price`	`a.price > 0`	Positive price (filter out sentinel `price = 0`)
`buy_crosses_ask`	`a.side = 1 && s.best_ask > 0 && a.price >= s.best_ask`	Buy is marketable against the resting ask
`sell_crosses_bid`	`a.side = 2 && s.best_bid > 0 && a.price <= s.best_bid`	Sell is marketable against the resting bid

no_trades_yet and has_traded together exhaustively partition the integers num_trades can take — that matters for reachability. Without the partition, the solver can pick a witness with num_trades < 0 (formally valid IML but uncovered by any scenario's given), which leaks into a sink.

Transitions

A single on_order transition handles all three sides. This is one of the cases where a monolithic branching transition is appropriate: the underlying source code (exchange/match.py) is itself one dispatch function, and the branches don't represent separately-named behavioral classes.

if a.side = 0 then
  { best_bid = 0; best_ask = 0;
    last_price = s.last_price; num_trades = s.num_trades }
else if a.side = 1 then
  (if s.best_ask > 0 && a.price >= s.best_ask then
     { best_bid = s.best_bid; best_ask = 0;
       last_price = s.best_ask; num_trades = s.num_trades + 1 }
   else if a.price > s.best_bid then
     { best_bid = a.price; best_ask = s.best_ask;
       last_price = s.last_price; num_trades = s.num_trades }
   else s)
else if a.side = 2 then
  (if s.best_bid > 0 && a.price <= s.best_bid then
     { best_bid = 0; best_ask = s.best_ask;
       last_price = s.best_bid; num_trades = s.num_trades + 1 }
   else if s.best_ask = 0 || a.price < s.best_ask then
     { best_bid = s.best_bid; best_ask = a.price;
       last_price = s.last_price; num_trades = s.num_trades }
   else s)
else s

Scenarios

Scenario	Given	When	Then	Flags
`init_resting_buy`	`book_empty`, `no_trades_yet`	`is_buy`, `valid_price`	`on_order`	`initial`
`init_resting_sell`	`book_empty`, `no_trades_yet`	`is_sell`, `valid_price`	`on_order`	`initial`
`trade_buy_lifts_ask`	`ask_only`	`is_buy`, `buy_crosses_ask`, `valid_price`	`on_order`	`goal`
`trade_sell_hits_bid`	`bid_only`	`is_sell`, `sell_crosses_bid`, `valid_price`	`on_order`	`goal`
`cancel_clears_book`	`bid_only`, `no_trades_yet`	`is_cancel`	`on_order`
`post_trade_book_empty`	`book_empty`, `has_traded`	—	—
`locked_book_violation`	`book_locked`	—	—	`bad`

Notes:

Two initial scenarios from book_empty cover the two possible first-order sides.
trade_* scenarios are marked goal — reachability checks confirm that a trade is achievable from the initial state.
post_trade_book_empty is an observation scenario with no when/then. Its only job is to act as an observed node in the reachability graph so the post-trade state (book_empty ∧ has_traded) doesn't appear as a sink. Without it, the trade scenarios would land in a sink and the post-trade state would never be visited again.
locked_book_violation is the bad scenario — the safety claim. Reachability should report this region as unreachable from any initial.

Reachability and safety

Run speclogician reach properties and you should see:

SAFE: locked_book_violation is unreachable from any initial.
LIVE: both trade_buy_lifts_ask and trade_sell_hits_bid are reachable.

The reachability graph traces the typical lifecycle:

book_empty (initial)
   ↓ init_resting_buy
bid_only
   ↓ trade_sell_hits_bid   ← goal
book_empty ∧ has_traded (post_trade_book_empty)

…and symmetrically for the ask side.

If you change the matching transition to accept a buy at price == best_ask + 1 while also leaving the resting ask in place (a real-world bug), the locked-book invariant would become reachable and reach safety would emit a counterexample path.

Related: this demo focuses on the lifecycle — orders resting, consuming on a match, the book cycling back to empty. For a complementary view focused on price-determination rules (the SIX Swiss matching rule book, with one transition + one scenario + one doc artifact per regulatory clause), see SIX Swiss match-price rules. That demo deliberately omits order consumption so the rule-by-rule structure stays visible — its graph terminates at the matching nodes rather than cycling.

Building this model with the CLI

Collect evidence

speclogician ch data doc-add --art-id doc-req \
  --text "Matching policy. An incoming buy at price p executes against the resting ask if best_ask > 0 and p >= best_ask, printing at the resting ask's price. Otherwise it rests on the book if p improves the bid. Sells are symmetric. Cancels clear the book." \
  --meta "Exchange matching policy, §3.2."
 
speclogician ch data src-add --art-id src-impl \
  --file-path "exchange/match.py" --language python \
  --src-code "def on_order(state, order): ..."

Define the model

# Domain base
speclogician ch base-edit --src "type state = { best_bid : int; best_ask : int; last_price : int; num_trades : int }
type action = { side : int; price : int; qty : int }"
 
# State predicates
speclogician ch pred-add --pred-type state --pred-name book_empty \
  --pred-src "s.best_bid = 0 && s.best_ask = 0"
speclogician ch pred-add --pred-type state --pred-name bid_only \
  --pred-src "s.best_bid > 0 && s.best_ask = 0"
speclogician ch pred-add --pred-type state --pred-name ask_only \
  --pred-src "s.best_bid = 0 && s.best_ask > 0"
speclogician ch pred-add --pred-type state --pred-name book_locked \
  --pred-src "s.best_bid > 0 && s.best_ask > 0 && s.best_bid >= s.best_ask" \
  --description "Crossed/locked book — the safety invariant says this must be unreachable."
speclogician ch pred-add --pred-type state --pred-name no_trades_yet \
  --pred-src "s.num_trades <= 0"
speclogician ch pred-add --pred-type state --pred-name has_traded \
  --pred-src "s.num_trades > 0"
 
# Action predicates
speclogician ch pred-add --pred-type action --pred-name is_buy   --pred-src "a.side = 1"
speclogician ch pred-add --pred-type action --pred-name is_sell  --pred-src "a.side = 2"
speclogician ch pred-add --pred-type action --pred-name is_cancel --pred-src "a.side = 0"
speclogician ch pred-add --pred-type action --pred-name valid_price --pred-src "a.price > 0"
speclogician ch pred-add --pred-type action --pred-name buy_crosses_ask \
  --pred-src "a.side = 1 && s.best_ask > 0 && a.price >= s.best_ask"
speclogician ch pred-add --pred-type action --pred-name sell_crosses_bid \
  --pred-src "a.side = 2 && s.best_bid > 0 && a.price <= s.best_bid"
 
# Transition (a single matching engine)
speclogician ch trans-add --trans-name on_order \
  --trans-src "if a.side = 0 then { best_bid = 0; best_ask = 0; last_price = s.last_price; num_trades = s.num_trades } else if a.side = 1 then (if s.best_ask > 0 && a.price >= s.best_ask then { best_bid = s.best_bid; best_ask = 0; last_price = s.best_ask; num_trades = s.num_trades + 1 } else if a.price > s.best_bid then { best_bid = a.price; best_ask = s.best_ask; last_price = s.last_price; num_trades = s.num_trades } else s) else if a.side = 2 then (if s.best_bid > 0 && a.price <= s.best_bid then { best_bid = 0; best_ask = s.best_ask; last_price = s.best_bid; num_trades = s.num_trades + 1 } else if s.best_ask = 0 || a.price < s.best_ask then { best_bid = s.best_bid; best_ask = a.price; last_price = s.last_price; num_trades = s.num_trades } else s) else s" \
  --description "Single matching transition: buys lift the ask, sells hit the bid; otherwise rest or no-op."
 
# Scenarios
speclogician ch scenario-add init_resting_buy \
  --given book_empty --given no_trades_yet \
  --when is_buy --when valid_price --then on_order --initial \
  --description "From empty book, first buy rests as the top-of-book bid."
speclogician ch scenario-add init_resting_sell \
  --given book_empty --given no_trades_yet \
  --when is_sell --when valid_price --then on_order --initial \
  --description "From empty book, first sell rests as the top-of-book ask."
 
speclogician ch scenario-add trade_buy_lifts_ask \
  --given ask_only --when is_buy --when buy_crosses_ask --when valid_price \
  --then on_order --goal \
  --description "An incoming buy that crosses the resting ask executes a trade."
speclogician ch scenario-add trade_sell_hits_bid \
  --given bid_only --when is_sell --when sell_crosses_bid --when valid_price \
  --then on_order --goal \
  --description "An incoming sell that crosses the resting bid executes a trade."
 
speclogician ch scenario-add cancel_clears_book \
  --given bid_only --given no_trades_yet \
  --when is_cancel --then on_order \
  --description "A cancel from a bid-only book clears the order."
 
speclogician ch scenario-add post_trade_book_empty \
  --given book_empty --given has_traded \
  --description "Observation scenario: book empty after at least one trade."
 
speclogician ch scenario-add locked_book_violation \
  --given book_locked --bad \
  --description "Safety invariant: a crossed/locked book is forbidden."
 
# Link artifacts
speclogician ch data link --art-id doc-req --comp-name locked_book_violation
speclogician ch data link --art-id src-impl --comp-name on_order
# … link doc-req to each scenario; src-impl to on_order

Inspect and verify

speclogician view state --compact
speclogician reach summary       # node/edge counts
speclogician reach properties    # SAFE + LIVE check
speclogician reach safety        # specifically: is locked_book_violation reachable?

Expected:

book_locked ∧ ¬book_empty is unreachable from any initial — the matching transition never produces a crossed book.
Both trade_* scenarios are reachable — confirming the system can actually execute trades.
The dashboard's reachability graph shows the two initial nodes (book_empty ∧ no_trades_yet), the resting-order intermediate nodes (bid_only, ask_only), and the post-trade observation node — with the locked-book node visibly disconnected from the rest.