Tlaplus Spec Generator

TLA+ Spec Generator

Automatically generate TLA+ specifications from program implementations for formal verification of distributed systems.

Overview

This skill transforms imperative programs (C/C++, Python) into declarative TLA+ specifications. It analyzes program structure to identify state variables, actions, and system behavior, then generates well-structured TLA+ modules suitable for model checking with TLC.

Workflow

1. Analyze Source Code

Generate TLA+ specification from source files:

# Single file
python3 scripts/generate_spec.py program.py -o Spec.tla

# Multiple files
python3 scripts/generate_spec.py server.py client.py protocol.py -o Protocol.tla

# With module name
python3 scripts/generate_spec.py distributed_system.c -o System.tla --module-name DistributedSystem

The generator automatically:

• Detects programming language
• Parses source code
• Identifies state variables and actions
• Extracts system structure
• Generates TLA+ specification

2. Specify System Parameters

For distributed systems, specify the number of processes:

python3 scripts/generate_spec.py consensus.py -o Consensus.tla --processes 3

This creates a constant N in the TLA+ spec representing the number of processes/nodes.

3. Generated Output

The generator produces two files:

1. Spec.tla - Complete TLA+ specification:

---- MODULE Spec ----
EXTENDS Naturals, Sequences, FiniteSets, TLC

CONSTANTS N  \* Number of processes

VARIABLES
  state,
  messages,
  committed

vars == <<state, messages, committed>>

TypeOK ==
  /\ state \in [1..N -> {"Init", "Working", "Done"}]
  /\ messages \in SUBSET Messages
  /\ committed \in SUBSET Operations

Init ==
  /\ state = [p \in 1..N |-> "Init"]
  /\ messages = {}
  /\ committed = {}

SendMessage(p, msg) ==
  /\ state[p] = "Working"
  /\ messages' = messages \cup {msg}
  /\ UNCHANGED <<state, committed>>

Next ==
  \/ \E p \in 1..N, msg \in Messages : SendMessage(p, msg)

Spec == Init /\ [][Next]_vars

====

2. Spec_mapping.txt - Explanation of program-to-TLA+ mapping:

• State variables and their types
• Actions and what they modify
• Processes identified
• Constants defined

4. Refine the Specification

The generated spec is a starting point. Refine it by:

• Review state variables - Ensure all relevant state is captured
• Complete action definitions - Add preconditions and effects
• Add invariants - Define safety properties
• Add temporal properties - Define liveness properties
• Adjust abstraction - Balance detail vs. tractability

5. Model Check with TLC

Create a TLC configuration file (Spec.cfg):

CONSTANTS
  N = 3

SPECIFICATION Spec

INVARIANT TypeOK

Run TLC model checker:

tlc Spec.tla -config Spec.cfg

Abstraction Levels

Control the level of abstraction:

# Low abstraction (more detail, larger state space)
python3 scripts/generate_spec.py program.py -o Spec.tla --abstraction low

# Medium abstraction (balanced, recommended)
python3 scripts/generate_spec.py program.py -o Spec.tla --abstraction medium

# High abstraction (minimal states, protocol-level)
python3 scripts/generate_spec.py program.py -o Spec.tla --abstraction high

Medium abstraction (default):

• Booleans → preserved
• Integers → bounded ranges (0..N)
• Enums → preserved as string sets
• Collections → sequences or sets
• Focus on control flow and key state

Common Use Cases

Distributed Consensus Protocol

Scenario: Implementing Raft or Paxos consensus algorithm.

Approach:

• Generate spec from implementation
• Identify processes (nodes), state variables (term, log, votes)
• Extract actions (RequestVote, AppendEntries, etc.)
• Add safety properties (leader uniqueness, log consistency)
• Verify with TLC

See: distributed_patterns.md

Message-Passing System

Scenario: Distributed system with processes communicating via messages.

Approach:

• Generate spec from message handlers
• Model network as set of messages in transit
• Define Send and Receive actions
• Add properties (message ordering, delivery guarantees)
• Check for deadlocks and livelocks

See: distributed_patterns.md

Replication Protocol

Scenario: Primary-backup or multi-master replication.

Approach:

• Generate spec from replication logic
• Model replicas and their logs
• Define replication and commit actions
• Add consistency properties
• Verify under failures

See: distributed_patterns.md

Leader Election

Scenario: Implementing leader election algorithm.

Approach:

• Generate spec from election code
• Model process states (follower, candidate, leader)
• Extract election actions
• Add safety (at most one leader) and liveness (eventually a leader)
• Verify correctness

See: distributed_patterns.md

Advanced Options

Focus on Specific Functions

Extract only relevant functions:

python3 scripts/generate_spec.py system.py -o Spec.tla \
  --focus-functions send_message receive_message commit_transaction

Track Specific Variables

Explicitly specify state variables:

python3 scripts/generate_spec.py system.py -o Spec.tla \
  --track-vars state messages committed_ops leader_id

Refining Generated Specs

Generated specs need refinement. Common refinements:

1. Complete action preconditions:

\* Generated (incomplete)
SendMessage(p, msg) ==
  /\ messages' = messages \cup {msg}

\* Refined (with precondition)
SendMessage(p, msg) ==
  /\ state[p] = "Active"        \* Precondition
  /\ msg \notin messages         \* No duplicates
  /\ messages' = messages \cup {msg}
  /\ UNCHANGED <<state, committed>>

2. Add invariants:

\* Safety properties
SafetyInvariant ==
  /\ \A p \in Procs : state[p] \in ValidStates
  /\ Cardinality({p \in Procs : state[p] = "Leader"}) <= 1

\* Add to spec
INVARIANT TypeOK
INVARIANT SafetyInvariant

3. Add liveness properties:

\* Eventually reach consensus
PROPERTY <>[](\A p \in Procs : state[p] = "Committed")

\* Every request is eventually processed
PROPERTY \A req \in Requests : [](Submitted(req) => <>Processed(req))

4. Add fairness:

\* Weak fairness: continuously enabled actions eventually happen
Spec == Init /\ [][Next]_vars /\ WF_vars(ReceiveMessage)

\* Strong fairness: infinitely often enabled actions eventually happen
Spec == Init /\ [][Next]_vars /\ SF_vars(ElectLeader)

Tips

• Start with small models - Use N=2 or N=3 processes initially
• Check TypeOK first - Ensures basic correctness before complex properties
• Use symmetry - Add SYMMETRY Permutations(Procs) to reduce state space
• Abstract data values - Focus on protocol behavior, not data content
• Iterate abstraction - If TLC is too slow, increase abstraction
• Read the mapping file - Understand how program maps to TLA+
• Consult patterns - See reference docs for common distributed system patterns

Common Issues

State explosion: TLC runs out of memory or takes too long.

• Solution: Increase abstraction, reduce N, add state constraints, use symmetry

Deadlock detected: TLC finds states with no enabled actions.

• Solution: Check action preconditions, ensure progress is always possible, add fairness

Invariant violated: TLC finds counterexample.

• Solution: Review counterexample trace, fix implementation or weaken invariant

Spec too abstract: Properties are trivially true.

• Solution: Decrease abstraction, track more variables, preserve more detail

References

• tlaplus_syntax.md: Complete TLA+ syntax reference with examples
• distributed_patterns.md: Common patterns for distributed systems (consensus, replication, leader election)

Scripts

• generate_spec.py: Main generation script (orchestrates entire process)
• program_analyzer.py: Program analysis module (extracts state, actions, processes)
• tlaplus_generator.py: TLA+ generation module (produces TLA+ specifications)

External Tools

• TLA+ Toolbox: IDE for writing and checking TLA+ specs (https://lamport.azurewebsites.net/tla/toolbox.html)
• TLC Model Checker: Command-line model checker (included with Toolbox)
• TLAPS: TLA+ Proof System for theorem proving (optional)