Building Your First Formal Model

You’ve read that formal methods find bugs testing misses. You understand the theory. But when you sit down to write your first specification, the blank editor stares back. Where do you start? This guide walks through the complete process: starting with a simple program, identifying what to model, building specifications in both TLA+ and Alloy, and running verification. By the end, you’ll have written working formal models and found a real bug. Let’s model something familiar: a login system with lockout protection. Here’s the pseudocode:

MAX_ATTEMPTS = 3

state = "logged_out"
failed_attempts = 0

function attempt_login(password):
    if state == "locked":
        return "account locked"

    if state == "logged_in":
        return "already logged in"

    if password == correct_password:
        state = "logged_in"
        failed_attempts = 0
        return "success"
    else:
        failed_attempts = failed_attempts + 1
        if failed_attempts >= MAX_ATTEMPTS:
            state = "locked"
        return "invalid password"

function logout():
    if state == "logged_in":
        state = "logged_out"
        return "logged out"
    return "not logged in"

function reset_lockout():  # Admin action
    if state == "locked":
        state = "logged_out"
        failed_attempts = 0

Simple enough. Three states, a counter, some transitions. What could go wrong?

Step 1: Identify States and Transitions

Before writing any specification, sketch the state machine on paper. What are the possible states? What causes transitions between them? States:

logged_out - initial state, can attempt login
logged_in - authenticated, can logout
locked - too many failed attempts, blocked until admin reset

Transitions:

logged_out → logged_in (correct password)
logged_out → locked (third wrong password)
logged_in → logged_out (logout)
locked → logged_out (admin reset)

Variables:

state - current authentication state
failed_attempts - counter (0-3)

Already questions emerge. What happens if someone tries to login while already logged in? What if there’s a race condition between login attempts? Can failed_attempts ever exceed MAX_ATTEMPTS? Formal modeling forces you to answer these questions precisely.

Step 2: Define Properties to Verify

What should be true about this system? Write these in plain English first: Safety properties (bad things that should never happen):

A user should never be in logged_in state without providing the correct password
failed_attempts should never exceed MAX_ATTEMPTS
A locked account should not allow login (we’ll see this is guaranteed structurally)

Liveness properties (good things that should eventually happen): 4. A user with the correct password should eventually be able to log in 5. A locked account should eventually be resettable This tutorial focuses on safety properties. Liveness requires fairness assumptions (guaranteeing certain actions eventually occur) and temporal operators like <> (eventually), covered in the TLA+ Syntax Guide. Now let’s translate safety properties into formal specifications.

TLA+ Specification

TLA+ models systems as state machines: an initial state, and actions that transition between states. Here’s our login system:

---------------------------- MODULE LoginSystem ----------------------------
EXTENDS Integers

CONSTANTS MaxAttempts

VARIABLES state, failedAttempts, lastInput

vars == <<state, failedAttempts, lastInput>>

States == {"logged_out", "logged_in", "locked"}

TypeInvariant ==
    /\ state \in States
    /\ failedAttempts \in 0..MaxAttempts
    /\ lastInput \in {"correct", "wrong", "none"}
----------------------------------------------------------------------------
Init ==
    /\ state = "logged_out"
    /\ failedAttempts = 0
    /\ lastInput = "none"

The Init predicate defines the starting state. The TypeInvariant constrains variables to valid ranges. If verification ever finds a state outside these bounds, something is wrong with our model.

Modeling Actions

Each action in TLA+ is a predicate describing when it can happen (precondition) and what changes (postcondition). Unprimed variables refer to the current state; primed variables (state') refer to the next state.

AttemptLoginCorrect ==
    /\ state = "logged_out"
    /\ state' = "logged_in"
    /\ failedAttempts' = 0
    /\ lastInput' = "correct"

AttemptLoginWrong ==
    /\ state = "logged_out"
    /\ failedAttempts' = failedAttempts + 1
    /\ lastInput' = "wrong"
    /\ IF failedAttempts' >= MaxAttempts
       THEN state' = "locked"
       ELSE state' = "logged_out"

Logout ==
    /\ state = "logged_in"
    /\ state' = "logged_out"
    /\ UNCHANGED failedAttempts
    /\ lastInput' = "none"

AdminReset ==
    /\ state = "locked"
    /\ state' = "logged_out"
    /\ failedAttempts' = 0
    /\ lastInput' = "none"

Notice AttemptLoginWrong checks the threshold against failedAttempts' (the post-increment value), not the original.

The Complete Specification

Next ==
    \/ AttemptLoginCorrect
    \/ AttemptLoginWrong
    \/ Logout
    \/ AdminReset

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

Next is the disjunction of all possible actions; any one can happen at each step. Spec says: start in Init, then repeatedly take Next steps (or stutter, staying in the same state).

Safety Properties in TLA+

Now we formalize our safety properties as invariants:

\* Property 1: Can't be logged in without correct password
\* (We track this by checking lastInput when entering logged_in)
NoUnauthorizedLogin ==
    state = "logged_in" => lastInput = "correct"

\* Property 2: Counter never exceeds maximum
CounterBounded ==
    failedAttempts <= MaxAttempts

These are state invariants: predicates that must hold in every reachable state. TLC checks them exhaustively. What about “can’t login from locked”? We don’t need an explicit invariant because it’s guaranteed by the action definitions. No action has both state = "locked" as a precondition and state' = "logged_in" as a postcondition. The structure of Next makes this transition impossible. This is a key insight: well-designed actions can make certain invariants unnecessary.

Running TLC

Create a model configuration file or use the TLA+ Toolbox:

CONSTANTS
    MaxAttempts = 3

SPECIFICATION Spec

INVARIANT TypeInvariant
INVARIANT CounterBounded
INVARIANT NoUnauthorizedLogin

Note: We model password correctness abstractly -AttemptLoginCorrect and AttemptLoginWrong are separate actions rather than checking an actual password value. This abstraction keeps the model simple while capturing the essential behavior.

Complete runnable specification

---------------------------- MODULE LoginSystem ----------------------------
EXTENDS Integers

CONSTANTS MaxAttempts

VARIABLES state, failedAttempts, lastInput

vars == <<state, failedAttempts, lastInput>>

States == {"logged_out", "logged_in", "locked"}

TypeInvariant ==
    /\ state \in States
    /\ failedAttempts \in 0..MaxAttempts
    /\ lastInput \in {"correct", "wrong", "none"}
----------------------------------------------------------------------------
Init ==
    /\ state = "logged_out"
    /\ failedAttempts = 0
    /\ lastInput = "none"

AttemptLoginCorrect ==
    /\ state = "logged_out"
    /\ state' = "logged_in"
    /\ failedAttempts' = 0
    /\ lastInput' = "correct"

AttemptLoginWrong ==
    /\ state = "logged_out"
    /\ failedAttempts' = failedAttempts + 1
    /\ lastInput' = "wrong"
    /\ IF failedAttempts' >= MaxAttempts
       THEN state' = "locked"
       ELSE state' = "logged_out"

Logout ==
    /\ state = "logged_in"
    /\ state' = "logged_out"
    /\ UNCHANGED failedAttempts
    /\ lastInput' = "none"

AdminReset ==
    /\ state = "locked"
    /\ state' = "logged_out"
    /\ failedAttempts' = 0
    /\ lastInput' = "none"

Next ==
    \/ AttemptLoginCorrect
    \/ AttemptLoginWrong
    \/ Logout
    \/ AdminReset

Spec == Init /\ [][Next]_vars
----------------------------------------------------------------------------
NoUnauthorizedLogin ==
    state = "logged_in" => lastInput = "correct"

CounterBounded ==
    failedAttempts <= MaxAttempts
============================================================================

Run TLC. With MaxAttempts = 3, it explores every reachable state in milliseconds. Result: All properties hold. The model checker proves that no sequence of actions can violate our invariants.

Finding a Bug: Shared State

The single-user model works. But what about concurrent access? Let’s extend the model for two users trying to authenticate simultaneously.

--------------------------- MODULE LoginSystemConcurrent ---------------------------
EXTENDS Integers

CONSTANTS MaxAttempts, Users

VARIABLES state, failedAttempts, activeUser

vars == <<state, failedAttempts, activeUser>>

Init ==
    /\ state = "logged_out"
    /\ failedAttempts = 0
    /\ activeUser = "none"

AttemptLoginWrong(u) ==
    /\ state = "logged_out"
    /\ activeUser' = u
    /\ failedAttempts' = failedAttempts + 1
    /\ IF failedAttempts' >= MaxAttempts
       THEN state' = "locked"
       ELSE state' = "logged_out"

AttemptLoginCorrect(u) ==
    /\ state = "logged_out"
    /\ state' = "logged_in"
    /\ failedAttempts' = 0
    /\ activeUser' = u

AdminReset ==
    /\ state = "locked"
    /\ state' = "logged_out"
    /\ failedAttempts' = 0
    /\ UNCHANGED activeUser

\* Any user can attempt login at any step
Next ==
    \/ \E u \in Users: AttemptLoginWrong(u)
    \/ \E u \in Users: AttemptLoginCorrect(u)
    \/ AdminReset

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

Note that this model has no invariants and omits Logout, deliberately. It’s a minimal model focused on login attempts to demonstrate that passing invariants doesn’t mean the design is correct. With Users = {"alice", "bob"} and MaxAttempts = 3, run TLC in simulation mode (or examine the state graph in the TLA+ Toolbox). Since no invariant is violated, TLC won’t produce an error trace automatically, but simulation shows possible behaviors. Here’s one trace you might observe:

State 1: failedAttempts = 0, state = "logged_out"
State 2: alice attempts wrong password, failedAttempts = 1
State 3: bob attempts wrong password, failedAttempts = 2
State 4: alice attempts wrong password, failedAttempts = 3, state = "locked"

Alice gets locked out after only two of her attempts because Bob’s attempt counted against her. The invariant failedAttempts <= MaxAttempts still holds (the counter reaches 3, not 4). But the design is broken: lockout punishes the wrong user. To catch this formally, we’d need a per-user invariant. But even without one, exploring the state space reveals the flaw. This is a key insight: formal modeling exposes design issues even when invariants pass. The fix: failedAttempts should be a function mapping users to their individual counters. Formal modeling found this before any code was written.

Alloy Specification

Alloy approaches the same problem differently. Instead of exploring state transitions, it searches for structural configurations that satisfy (or violate) constraints. Alloy 6 adds temporal operators, but let’s start with pure structural analysis.

module LoginSystem

abstract sig State {}
one sig LoggedOut, LoggedIn, Locked extends State {}

sig User {
    currentState: one State,
    failedAttempts: one Int
}

Each User has a currentState and a failedAttempts counter. Alloy will search for configurations (assignments of values to these fields) that satisfy our constraints. Note on integers: Alloy’s Int is bounded by bitwidth (default 4 bits: -8 to 7). For small counters like failedAttempts, this is fine. For larger values, specify a higher bitwidth with run ... for 5 Int or use a custom sig instead of Int.

Facts as Constraints

Alloy uses fact blocks to constrain valid configurations:

fact FailedAttemptsNonNegative {
    all u: User | u.failedAttempts >= 0
}

fact LockedMeansMaxAttempts {
    all u: User | u.currentState = Locked implies u.failedAttempts >= 3
}

fact LoggedInMeansNoFailures {
    all u: User | u.currentState = LoggedIn implies u.failedAttempts = 0
}

These facts define what configurations are valid. LockedMeansMaxAttempts ensures lockout only happens after three failures. LoggedInMeansNoFailures ensures the counter resets on successful login. Notice we don’t cap failedAttempts; the counter can keep incrementing after lockout.

Finding Counterexamples

The power of Alloy is asking “can this bad thing happen?” Let’s see what happens when we forget a constraint. First, temporarily comment out the LoggedInMeansNoFailures fact (prefix with --). Then add this predicate and run command:

-- Can a user be logged in with failed attempts > 0?
pred LoggedInWithFailures {
    some u: User | u.currentState = LoggedIn and u.failedAttempts > 0
}

run LoggedInWithFailures for 3

Running this shows SAT (yes, it’s possible). Alloy displays the instance: a user in LoggedIn state with failedAttempts = 2. Without the LoggedInMeansNoFailures constraint, nothing prevents this invalid configuration. Now restore the fact (remove the --) and run again: UNSAT. The bad configuration is now impossible. This workflow (remove a constraint, see what breaks, add it back) helps you understand what each constraint contributes.

Checking Assertions

Turn properties into assertions that Alloy tries to disprove:

-- If locked, must have hit max attempts
assert LockedImpliesMaxAttempts {
    all u: User | u.currentState = Locked implies u.failedAttempts = 3
}

check LockedImpliesMaxAttempts for 5

If Alloy finds a counterexample, it shows exactly how the assertion fails. Here it will find one: our fact says failedAttempts >= 3, not = 3. A locked user could have failedAttempts = 5 (satisfies the fact) but violates the assertion. This reveals a modeling decision: should the counter stop at 3 or keep incrementing? A more useful assertion:

-- Logged-in users have clean slate
assert CleanLogin {
    all u: User | u.currentState = LoggedIn implies u.failedAttempts = 0
}

check CleanLogin for 5

This passes because our LoggedInMeansNoFailures fact guarantees it. Assertions let you verify that facts actually enforce the properties you intend.

Complete runnable structural specification

module LoginSystem

abstract sig State {}
one sig LoggedOut, LoggedIn, Locked extends State {}

sig User {
    currentState: one State,
    failedAttempts: one Int
}

fact FailedAttemptsNonNegative {
    all u: User | u.failedAttempts >= 0
}

fact LockedMeansMaxAttempts {
    all u: User | u.currentState = Locked implies u.failedAttempts >= 3
}

fact LoggedInMeansNoFailures {
    all u: User | u.currentState = LoggedIn implies u.failedAttempts = 0
}

-- Predicate for exploring: comment out LoggedInMeansNoFailures to see SAT
pred LoggedInWithFailures {
    some u: User | u.currentState = LoggedIn and u.failedAttempts > 0
}

run LoggedInWithFailures for 3

assert LockedImpliesMaxAttempts {
    all u: User | u.currentState = Locked implies u.failedAttempts >= 3
}

check LockedImpliesMaxAttempts for 5

assert CleanLogin {
    all u: User | u.currentState = LoggedIn implies u.failedAttempts = 0
}

check CleanLogin for 5

Temporal Properties in Alloy 6

Alloy 6 adds temporal operators for behavioral modeling. To use them, mark fields with var:

module LoginSystemTemporal

open util/integer  -- for plus, minus, etc.

abstract sig State {}
one sig LoggedOut, LoggedIn, Locked extends State {}

sig User {
    var currentState: one State,
    var failedAttempts: one Int
}

-- Initial state: all users logged out with zero failures
pred init {
    all u: User | u.currentState = LoggedOut and u.failedAttempts = 0
}

-- Frame condition: fields of uninvolved users stay the same
pred frame[u: User] {
    all v: User - u |
        v.currentState' = v.currentState and
        v.failedAttempts' = v.failedAttempts
}

-- Transition: user enters wrong password
pred wrongPassword[u: User] {
    u.currentState = LoggedOut
    u.failedAttempts' = plus[u.failedAttempts, 1]
    (u.failedAttempts' >= 3 implies u.currentState' = Locked)
    (u.failedAttempts' < 3 implies u.currentState' = LoggedOut)
    frame[u]
}

-- Transition: user enters correct password
pred correctPassword[u: User] {
    u.currentState = LoggedOut
    u.currentState' = LoggedIn
    u.failedAttempts' = 0
    frame[u]
}

-- Transition: user logs out
pred logout[u: User] {
    u.currentState = LoggedIn
    u.currentState' = LoggedOut
    u.failedAttempts' = u.failedAttempts
    frame[u]
}

-- Transition: admin resets a locked account
pred adminReset[u: User] {
    u.currentState = Locked
    u.currentState' = LoggedOut
    u.failedAttempts' = 0
    frame[u]
}

-- System can always do something (stutter if nothing else)
pred stutter {
    all u: User |
        u.currentState' = u.currentState and
        u.failedAttempts' = u.failedAttempts
}

pred trans {
    (some u: User | wrongPassword[u] or correctPassword[u] or logout[u] or adminReset[u]) or stutter
}

fact Traces {
    init
    always trans
}

-- Safety: locked users stay locked until reset
assert LockPersists {
    always (all u: User |
        u.currentState = Locked implies
            (u.currentState' = Locked or adminReset[u]))
}

check LockPersists for 3 but 10 steps

The var keyword marks mutable fields. The always operator and primed variables (currentState') enable behavioral specification similar to TLA+. Key patterns in Alloy 6 temporal mode:

Frame conditions: Explicitly state what doesn’t change. Without frame[u], uninvolved users could change arbitrarily.
Stutter steps: Allow the system to remain in its current state. Alloy 6 traces are infinite. Without stutter, if no action is enabled, no valid trace exists and analysis returns UNSAT.
Init predicate: Constrains only the first state. The always trans requires a valid transition in every state; stutter ensures one always exists.
Step bounds: but 10 steps limits trace length for bounded model checking.

Comparing the Approaches

Aspect	TLA+	Alloy (structural)	Alloy 6 (temporal)
Model	State transitions	Structural constraints	State transitions
Finds	Execution traces that violate properties	Configurations that violate assertions	Traces or configurations
Strength	Temporal sequences, liveness	Counterexample visualization	Both structural and temporal
Output	Step-by-step trace	Visual graph of instance	Visual trace or graph

Alloy 6 added temporal operators (var, always, primed variables), giving it TLA+-like capabilities. The structural mode remains powerful for exploring data models; the temporal mode enables behavioral verification. Use TLA+ when you care about sequences: “Does every lockout eventually get reset?” requires temporal reasoning about what must happen over time. Use Alloy structural mode when you care about structure: “Can a locked user have zero failed attempts?” is a constraint satisfaction question. Use Alloy temporal mode when you want both: behavioral verification with Alloy’s visualization and relational operators. For the login system, each tool revealed different aspects. TLA+ exposed the shared-counter flaw through state exploration. Alloy exposed missing constraints by finding configurations we hadn’t explicitly forbidden.

The Modeling Process

Here’s the general workflow, now that you’ve seen it in action:

Sketch the state space. What are the states? What are the transitions? Draw it on paper first.
Identify variables. What data needs to be tracked? What are their valid ranges?
Write properties first. What should always be true? What should never happen? English first, then formalize.
Start simple. Single user, small constants. Get the basic model working before adding complexity.
Add complexity incrementally. Concurrency, multiple users, edge cases. Each addition may reveal new bugs.
Trust the counterexamples. When the model checker finds a violation, it’s real (in your model). Either fix the model or fix the design.

What We Found

Starting from simple pseudocode, formal modeling revealed:

Per-user vs. global counter ambiguity. The original design didn’t specify, so a real implementation might get it wrong.
Counter reset timing. Should failedAttempts reset on successful login? The code says yes, but did we test it?
Concurrent access behavior. Two users interleaving attempts breaks assumptions about lockout.

None of these required writing or running any code. The formal model exposed design issues before implementation began.

Next Steps

You’ve built your first formal model. Here’s where to go next: Deepen your TLA+ knowledge. The TLA+ Basics guide covers temporal operators, fairness, and more complex examples. Explore Alloy’s relational power. The Alloy Basics guide demonstrates structural modeling with file systems and permissions. Model something real. Pick a system you work with. A queue processor. A permission system. An API state machine. The act of modeling will reveal assumptions you didn’t know you were making. The login system was 30 lines of pseudocode. The formal model was about the same size. But the model checked millions of states and found bugs that testing would likely miss. That’s the value proposition: similar effort, much stronger guarantees.

Complete specifications from this guide are available in the examples repository. Download MacTLA or MacAlloy to run them locally.

Overview

TLA+

Alloy

AD Tier Model Specifications

Binary Analysis Series

Malware Analysis

Aviation Systems Series

Tools

Building Your First Formal Model

Step 1: Identify States and Transitions

Step 2: Define Properties to Verify

TLA+ Specification

Modeling Actions

The Complete Specification

Safety Properties in TLA+

Running TLC

Finding a Bug: Shared State

Alloy Specification

Facts as Constraints

Finding Counterexamples

Checking Assertions

Temporal Properties in Alloy 6

Comparing the Approaches

The Modeling Process

What We Found

Next Steps

​The Program: A Login System

​Step 1: Identify States and Transitions

​Step 2: Define Properties to Verify

​TLA+ Specification

​Modeling Actions

​The Complete Specification

​Safety Properties in TLA+

​Running TLC

​Finding a Bug: Shared State

​Alloy Specification

​Facts as Constraints

​Finding Counterexamples

​Checking Assertions

​Temporal Properties in Alloy 6

​Comparing the Approaches

​The Modeling Process

​What We Found

​Next Steps

The Program: A Login System

Step 1: Identify States and Transitions

Step 2: Define Properties to Verify

TLA+ Specification

Modeling Actions

The Complete Specification

Safety Properties in TLA+

Running TLC

Finding a Bug: Shared State

Alloy Specification

Facts as Constraints

Finding Counterexamples

Checking Assertions

Temporal Properties in Alloy 6

Comparing the Approaches

The Modeling Process

What We Found

Next Steps