Formal Verification

wirespec verifies state machines at two levels: static analysis at compile time, and TLA+ model checking for deeper properties.

By default, wirespec verify runs a built-in Rust model checker (tla-checker) automatically -- no Java installation required. For larger state spaces, you can optionally use the external Java-based TLC model checker via --run-tlc.

Static Analysis

The compiler automatically checks these properties for every state machine:

Check	What it detects
Terminal irreversibility	Transitions out of [terminal] states
Delegate acyclicity	Circular delegation chains between state machines
Structural reachability	States that can never reach a terminal state
Exhaustive transitions	Non-terminal states with no outgoing transitions
Wildcard priority	Correct override of wildcard by concrete transitions

These checks run at compile time with zero configuration.

TLA+ Model Checking

For deeper verification, wirespec generates TLA+ specifications and runs the built-in model checker.

Declaring Properties

Add verify declarations inside your state machine:

@verify(bound = 3)
state machine PathState {
    state Init { path_id: u8 }
    state Active { path_id: u8, rtt: u8 = 0 }
    state Closed [terminal]
    initial Init

    transition Init -> Active {
        on activate(id: u8)
        action { dst.path_id = src.path_id; }
    }
    transition Active -> Closed { on close }
    transition * -> Closed { on abort }

    verify NoDeadlock
    verify AllReachClosed
    verify property AbandonIsFinal:
        in_state(Closing) -> [] not in_state(Active)
}

Built-in Properties

Property	Type	What it checks
NoDeadlock	Safety (invariant)	Every non-terminal state has at least one enabled transition
AllReachClosed	Liveness	Under fair scheduling, all paths eventually reach a terminal state

User-defined Properties

Use temporal logic operators in verify property:

Operator	Meaning	Example
[]	Always (globally)	[] not in_state(Error)
<>	Eventually	<> in_state(Closed)
~>	Leads to	in_state(Active) ~> in_state(Closed)
->	Implies	in_state(B) -> not in_state(A)
and / or / not	Logical	in_state(A) and not in_state(B)
in_state(S)	State predicate	in_state(Active)

Running Verification

# Default: generate TLA+ specs and run built-in Rust model checker (no Java needed)
wirespec verify path.wspec -o build/tla/

# Use external Java TLC instead (for large state spaces)
wirespec verify path.wspec --run-tlc --bound 3

The Bound Parameter

@verify(bound = N) controls the size of the value domains for model checking. Each integer field ranges over 0..N-1. Larger bounds explore more states but take longer.

Bound	States explored	Time
2	~100	< 1s
3	~1,000	~1s
5	~10,000	~5s

CLI --bound N overrides the annotation.

Guard Exclusivity

When multiple transitions share the same (state, event) pair with different guards, wirespec automatically generates a TLA+ invariant to verify the guards are mutually exclusive:

transition Trying -> Trying {
    on retry
    guard src.count < 3
    action { dst.count = src.count + 1; }
}
transition Trying -> Done {
    on retry
    guard src.count >= 3
}

The model checker verifies that count < 3 and count >= 3 never hold simultaneously.

Verifying Hierarchical State Machines

State machines that use delegate can also be verified. wirespec inlines the child state machine's states and transitions into the parent's TLA+ spec, so the model checker explores the combined parent-child state space in a single pass.

state machine Child {
    state Idle {}
    state Done [terminal]
    initial Idle
    transition Idle -> Done { on finish }
}

state machine Parent {
    state Running { child: Child }
    state Closed [terminal]
    initial Running

    transition Running -> Running {
        on forward(ev: u8)
        delegate src.child <- ev
    }
    transition Running -> Closed {
        on child_state_changed
        guard src.child in_state(Done)
    }

    verify NoDeadlock
    verify AllReachClosed
}

wirespec verify parent.wspec

The generated TLA+ spec tracks the child's state as a field in the parent's state record. A ChildDispatch operator maps event ordinals to child transitions, and child_state_changed transitions fire when the child's state changes.

This also works for arrays of child state machines:

state machine Connection {
    state Open { paths: [PathState; 4] }
    state Done [terminal]
    initial Open

    transition Open -> Open {
        on close_path(idx: u8, ev: u8)
        delegate src.paths[idx] <- ev
    }
    transition Open -> Done { on shutdown }
    verify NoDeadlock
}

The bound parameter applies to both parent and child value domains. Keep in mind that arrays of child state machines multiply the state space — use a small bound (2 or 3) to keep verification tractable.

Currently, only one level of delegation is supported for verification. If a child state machine itself uses delegate, wirespec verify will report an error.