formal-spec

Formal Specification Workflow with TLX

TLX enables formal verification of state machines by writing declarative specs in Elixir and model-checking them with TLC. This skill covers the full lifecycle: design-time abstract specs, implementation-time concrete specs, and CI-time refinement checking.

When to Use This Workflow

Apply formal specification to state machines with:

• Multiple states and guarded transitions
• Concurrent access or distributed coordination
• Safety properties ("this must never happen")
• Liveness properties ("this must eventually happen")
• Approval gates, quorum requirements, or sequencing constraints

Not every GenServer needs a spec. Target modules with complex state logic — :gen_statem, GenServers with explicit state machines, or any module where an ADR describes valid/invalid state transitions.

Phase 1: Abstract Spec from ADR

Read the ADR and extract

1. States — all named states the system can be in
2. Transitions — which events move between states, with guards
3. Forbidden transitions — state pairs that must never be directly reachable
4. Invariants — properties that must hold in every reachable state
5. Liveness — properties about eventual behavior (optional)

Write the abstract TLX spec

Every spec file starts with a cross-reference header:

# ADR: 0029, 0013
# Source: apps/forge_infra/lib/forge/firmware/orchestrator.ex

• ADR: — comma-separated ADR numbers this spec derives from
• Source: — relative path to the implementation (omit for abstract-only specs)

import TLX

defspec AbstractFirmware do
  variable :state, :idle

  action :begin do
    guard(e(state == :idle))
    next :state, :updating
  end

  action :complete do
    guard(e(state == :updating))
    next :state, :committed
  end

  action :fail do
    guard(e(state == :updating))
    next :state, :failed
  end

  invariant :committed_is_terminal,
            e(ite(state == :committed, true, true))
end