Examples

These examples demonstrate SpecLogician's modeling and reasoning capabilities across a range of domains. Each example first describes the model — domain types, predicates, transitions, and scenarios — then shows how to build it using speclogician CLI commands.

Every example below is also a runnable demo shipped with SpecLogician. Run any of them with speclogician demo run <id>, then open the result in the dashboard via speclogician demo dashboard <id> or the VS Code extension. The full list is also visible from the CLI via speclogician demo ls.

Available examples

The examples are ordered roughly by complexity — pick the first one you haven't seen before. Each one is a complete, working spec; copy-paste the build commands into your own project to reuse the patterns.

1. Order limits  ·  speclogician demo run order-limits
   Step-by-step formalization of an order quantity validation rule. The canonical starter spec: one predicate, one transition, two scenarios. Start here if you've never built a SpecLogician model.

2. Bank account  ·  speclogician demo run bank-account
   Deposits, withdrawals, freeze/unfreeze, and rejection paths. Demonstrates algebraic data types (variants for account status and operation kind), multi-operation modeling, and how rejection paths share a noop transition.

3. Traffic light  ·  speclogician demo run traffic-light
   A traffic light controller cycling Red → Green → Yellow → Red, with an emergency override that forces Red. A clean introduction to multi-phase state machines and how scenarios partition by (phase, signal) pairs.

4. Shopping cart  ·  speclogician demo run shopping-cart
   Add items, apply a one-time discount, checkout, cancel. Shows variant types for cart status, multiple transitions, and richer scenarios spanning both happy and rejection paths (double_discount, checkout_empty_cart, modify_after_checkout).

5. Boundary conflict  ·  speclogician demo run boundary-conflict
   Two requirements that disagree at the boundary (qty == 10000). Demonstrates conflict detection between scenarios and how to resolve it by refining predicates.

6. Handshake protocol  ·  speclogician demo run handshake
   A client must authenticate before entering the READY state. Demonstrates reachability constraints — proving that READY is unreachable without a successful auth.

7. Risk flag latch  ·  speclogician demo run risk-flag-latch
   A latched risk flag that blocks new orders until explicit reset. Demonstrates stateful guards and reachability through a mandatory intermediate step (reset is required to clear the latch).

8. Trace-driven modeling  ·  speclogician demo run trace-driven
   The reverse workflow: start from concrete test traces and production logs, extract predicates from observed values, and lift the traces into symbolic scenarios. Useful when there are no requirements docs and the only "spec" is observed behavior.

9. Stock exchange  ·  speclogician demo run stock-exchange
   A single-security top-of-book matching engine with a safety invariant against a crossed/locked book. The cleanest demo for showing how is_bad scenarios drive safety analysis — and how reachability reports SAFE / UNSAFE with a counterexample path.

10. SIX Swiss match-price rules  ·  speclogician demo run six-swiss
    The most regulation-heavy example. Each clause of the SIX Swiss matching rule book maps one-to-one to a named transition, scenario, and doc artifact (§3.2 Limit×Limit, §3.3 Market×Limit, §3.4 Market×Market, §3.5 Quote tie-breaking). Showcase of granular per-rule modeling — read this if you're formalizing a regulated domain.

How to read an example

Each page follows the same structure:

1. The system — informal description (what's the domain doing?).
2. Domain base — IML type definitions for state and action.
3. Predicates — state and action predicates with tables of name + IML body + meaning.
4. Transitions — one section per transition with its IML body and purpose.
5. Scenarios — tables grouped by intent (happy paths, rejection paths, safety claims).
6. Reachability / safety / complement — what the analysis tells you about the model.
7. Building this model with the CLI — copy-pasteable commands and an equivalent batch JSON.

The CLI command sequences in each example are the same commands the bundled demo's changes.py issues internally. Running speclogician demo run <id> simply replays that sequence into a fresh sl_state.json.

Beyond these examples

When you're ready to build your own spec:

• Generate the agent prompt with speclogician prompt and feed it to an LLM coding agent.
• Read the modeling-context docs for the conceptual model (predicates, transitions, scenarios).
• Read the reasoning-about-context docs for what the analysis layer does (consistency, reachability, complement).