> ## Documentation Index
> Fetch the complete documentation index at: https://docs.alchemicalchef.io/llms.txt
> Use this file to discover all available pages before exploring further.

# Building Your First Formal Model

> A step-by-step guide to translating a simple program into TLA+ and Alloy specifications

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.

## The Program: A Login System

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):

1. A user should never be in `logged_in` state without providing the correct password
2. `failed_attempts` should never exceed `MAX_ATTEMPTS`
3. 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](/formal-methods/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:

```tla theme={null}
---------------------------- 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.

```tla theme={null}
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

```tla theme={null}
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:

```tla theme={null}
\* 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.

<Accordion title="Complete runnable specification">
  ```tla theme={null}
  ---------------------------- 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
  ============================================================================
  ```
</Accordion>

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.

```tla theme={null}
--------------------------- 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.

```alloy theme={null}
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:

```alloy theme={null}
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:

```alloy theme={null}
-- 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:

```alloy theme={null}
-- 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:

```alloy theme={null}
-- 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.

<Accordion title="Complete runnable structural specification">
  ```alloy theme={null}
  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
  ```
</Accordion>

### Temporal Properties in Alloy 6

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

```alloy theme={null}
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:

1. **Sketch the state space.** What are the states? What are the transitions? Draw it on paper first.

2. **Identify variables.** What data needs to be tracked? What are their valid ranges?

3. **Write properties first.** What should always be true? What should never happen? English first, then formalize.

4. **Start simple.** Single user, small constants. Get the basic model working before adding complexity.

5. **Add complexity incrementally.** Concurrency, multiple users, edge cases. Each addition may reveal new bugs.

6. **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:

1. **Per-user vs. global counter ambiguity.** The original design didn't specify, so a real implementation might get it wrong.

2. **Counter reset timing.** Should `failedAttempts` reset on successful login? The code says yes, but did we test it?

3. **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](/formal-methods/tla-basics) guide covers temporal operators, fairness, and more complex examples.

**Explore Alloy's relational power.** The [Alloy Basics](/formal-methods/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](/formal-methods/mactla) or [MacAlloy](/formal-methods/macalloy) to run them locally.*