Model-Check a Job Processor with TLA+

Use TLA+ and TLC to find and fix a duplicate job charge race.

Introduction

30 Second Summary

A background job can look harmless until two workers grab it at nearly the same moment. A duplicate charge can reach a customer before the logs make the race obvious.

In this project, you will build two TLA+ models of workers racing to claim one job. TLC will expose a stale-read double charge in the first model before verifying the atomic repair in the second.

What You'll Build

You run the broken model to reveal a numbered duplicate-charge trace, then run the fixed model to see every reachable state pass the same at-most-once check.

By the end of this project, you'll have:

  • A runnable unsafe model that lets you reproduce a successful TypeOK check before testing the user-facing promise in AtMostOnce.
  • A concrete counterexample trace that lets you follow both workers reading the pending state before either worker records its charge.
  • A verified atomic model that checks every reachable state in the bounded two-worker scope. You can rerun it to see Model checking completed. No error has been found..
  • Secret Mission: Add a completion transition that TLC permits only after exactly one charge.

Are there any prerequisites?

You need Cursor on macOS plus basic familiarity with sets and Boolean logic. No prior TLA+ experience is required.

Before We Start

When two workers both read one pending job before either records its claim, each can charge it. In this project, you will use TLA+ to compare that unsafe race with an atomic claim-and-charge transition that preserves the at-most-once promise.

Set Up a Reproducible TLA+ Workspace

Your later counterexample only means something when another run can reproduce it. A pinned toolchain keeps every result tied to the same model checker.

The TLC model checker needs a compatible Java runtime. This project uses Microsoft Build of OpenJDK package 21.0.13.0.2.

You will also prepare Cursor with the TLA+ (Temporal Logic of Actions) extension. The project workspace will store its own TLC 1.7.4 JAR for repeatable terminal runs.

In this step, get ready to:
  • Verify the pinned Microsoft OpenJDK runtime.
  • Install the TLA+ Foundation extension in Cursor.
  • Create the project workspace with a pinned TLC JAR.
Verify the pinned Java runtime

A Java Virtual Machine runs the TLC JAR. Checking the active runtime first tells you whether the pinned OpenJDK build is already available.

  • Press Cmd+Space to open Spotlight.
  • Type Terminal in Spotlight.
  • Press Enter to open Terminal.
  • Check the active Java runtime by running this command:
java --version

What does this command do?

The command asks the active Java runtime to identify itself. Its output reveals whether your Mac can run the pinned TLC JAR.

✔️ I see the pinned build

Your output identifies Microsoft Build of OpenJDK 21.0.13 from package 21.0.13.0.2. Java is ready for TLC.

ⓧ I see an older version

Choosing the correct package can feel fiddly because Apple Silicon Macs use a different installer from Intel Macs. The package filename tells you which processor it supports.

  • Open the official Microsoft OpenJDK 21 download page.
  • Download microsoft-jdk-21.0.13.0.2-macos-aarch64.pkg if your Mac uses Apple Silicon.
  • Download microsoft-jdk-21.0.13.0.2-macos-x64.pkg if your Mac uses an Intel processor.
  • Open the downloaded PKG file from your Downloads folder in Finder.
  • Follow the installer prompts until the installation completes.
  • Return to Terminal from earlier.
  • Verify the newly installed runtime by running this command:
java --version

What should the version check show?

The installer makes its JDK tools available in your terminal path. The output should now identify Microsoft Build of OpenJDK 21.0.13.

ⓧ Command not found

Java is not available in your terminal path yet. Installing the native Microsoft package adds the JDK tools your model checker needs.

  • Open the official Microsoft OpenJDK 21 download page.
  • Download microsoft-jdk-21.0.13.0.2-macos-aarch64.pkg if your Mac uses Apple Silicon.
  • Download microsoft-jdk-21.0.13.0.2-macos-x64.pkg if your Mac uses an Intel processor.
  • Open the downloaded PKG file from your Downloads folder in Finder.
  • Follow the installer prompts until the installation completes.
  • Return to Terminal from earlier.
  • Verify the installed runtime by running this command:
java --version

What should the version check show?

The native installer adds the JDK tools to your terminal path. The output should now identify Microsoft Build of OpenJDK 21.0.13.

That is the first dependency locked down. Your Mac now has the pinned Java runtime required by TLC.

Java still unavailable?

  • Close Terminal after the installer finishes.
  • Open a fresh Terminal window before repeating the version check.
  • Confirm that the downloaded package matches your Mac processor.
  • Help me troubleshoot the OpenJDK installation.
Install the TLA+ extension

The extension gives Cursor syntax support for TLA+ modules. Confirming the publisher ensures you install the TLA+ Foundation release used by this project.

  • Press Cmd+Space to open Spotlight.
  • Type Cursor in Spotlight.
  • Press Enter to open Cursor.
  • Select Extensions in the left sidebar.
  • Enter TLA+ (Temporal Logic of Actions) in the extension search field.
  • Select the result published by TLA+ Foundation.
  • Select Install on the extension page.
  • Confirm that the installed extension shows version 1.7.0.

The extension now appears as installed in Cursor. Your editor is ready to recognize the TLA+ model files you create next.

Extension not installing?

  • Confirm that your Mac has an active internet connection.
  • Check that the selected extension is published by TLA+ Foundation.
  • Restart Cursor if the extension remains unavailable after installation.
  • Help me troubleshoot the TLA+ extension.
Build the pinned TLC workspace

The workspace keeps the deliberately racy model separate from its atomic repair. A dedicated tools directory stores the pinned model checker beside both model directories.

  • Switch back to Terminal from earlier.
  • Move to your Desktop by running this command:
cd ~/Desktop

Why use the Desktop?

The Desktop gives the project a predictable location on your Mac. You can reach the same folder easily from Terminal or Finder.

  • Create the workspace directories by running this command:
mkdir -p tla-job-processor/{tools,broken,fixed}

What does this command create?

  • The tla-job-processor directory holds the complete project.
  • The tools directory holds the pinned TLC JAR.
  • The broken directory is reserved for the deliberately racy model.
  • The fixed directory is reserved for the atomic corrected model.
  • Press Cmd+Space to open Spotlight.
  • Type Finder in Spotlight.
  • Press Enter to open Finder.
  • Select your Desktop in Finder.
  • Confirm that tla-job-processor contains tools, broken, and fixed.
  • Drag the tla-job-processor directory from Finder into the open Cursor window.
  • Approve the folder if Cursor asks for confirmation.

Good progress. Cursor now shows the tla-job-processor workspace with three empty directories.

Why use a separate TLC JAR?

A separately downloaded stable JAR makes the model-checking runtime explicit inside the project. Every later terminal command uses the same TLC release.

  • Open the official TLA+ stable release page.
  • Locate the stable release tagged v1.7.4.
  • Download the release asset named tla2tools.jar.
  • Return to Finder from earlier.
  • Open your Downloads folder in Finder.
  • Drag tla2tools.jar into the tools directory shown in Cursor.

You should now see tools/tla2tools.jar in the workspace. The broken and fixed directories remain empty.

  • Switch back to Terminal from earlier.
  • Move into the workspace by running this command:
cd ~/Desktop/tla-job-processor

Why change directories?

The verification command uses a path relative to the tla-job-processor directory. Moving there lets Java find the JAR at tools/tla2tools.jar.

Before you run the final check, do you expect TLC to print help or begin checking a model?

  • Verify the pinned TLC JAR by running this command:
java -jar tools/tla2tools.jar -help

What does this command do?

Java launches the JAR stored in the workspace. The -help option asks TLC to print its command-line help.

You should see TLC command-line help with its available options. This proves that Java can run the pinned tools/tla2tools.jar file from the project directory.

That is the setup complete. Cursor can edit your models while Terminal runs TLC 1.7.4 from the workspace itself.

TLC help not appearing?

  • Confirm that Terminal is inside the tla-job-processor directory.
  • Confirm that the downloaded file is named exactly tla2tools.jar.
  • Check that the JAR appears inside the tools directory in Cursor.
  • Help me troubleshoot the TLC help command.

✔️ Awesome, I've got everything!

Keep the tla-job-processor workspace open in Cursor. Your pinned Java and TLC toolchain is ready.

ⓧ I'd like to double check the full code

This setup step creates directories plus one binary JAR. Your workspace should match this exact checkpoint.

  • The broken/ directory is empty for the deliberately racy TLA+ model.
  • The fixed/ directory is empty for the atomic corrected TLA+ model.
  • The tools/tla2tools.jar file is the TLA+ Tools version 1.7.4 JAR downloaded from the official stable release.
  • The tools/tla2tools.jar file runs with Java from the tla-job-processor directory.

Your editor and pinned model checker are ready. Next, you will build the deliberately racy two-worker model and watch a type-only check pass.

Model the Racy Job Processor

Your pinned workspace can now run TLA+ models with TLC. The next challenge is to represent one pending job as a state machine that two workers can race through.

A model can keep every value in a valid shape while still breaking its user-facing promise. The first run checks only a type invariant.

The at-most-once promise stays outside that first check. This creates an intentionally incomplete baseline that looks successful.

In this step, get ready to:
  • Define the initial state for one job plus two workers.
  • Separate the pending read from the later charge commitment.
  • Run TLC with only TypeOK enabled.
Define the initial state

TLC explores every reachable state within the model's finite scope. The Workers set bounds this demonstration to two named workers.

  • In Cursor's file sidebar, select the broken directory.
  • Select the new-file control at the top of the file sidebar.
  • Name the file JobProcessor.tla.
  • Paste the initial state into broken/JobProcessor.tla using this code:
---- MODULE JobProcessor ----
EXTENDS FiniteSets

Workers == {"worker-1", "worker-2"}

VARIABLES claimed, observedPending, chargedBy
vars == <<claimed, observedPending, chargedBy>>

Init ==
    /\ claimed = FALSE
    /\ observedPending = {}
    /\ chargedBy = {}

====

What Does the Initial State Define?

  • The Workers set defines the complete worker population that TLC explores.
  • The claimed variable records whether the job has been claimed.
  • The observedPending set records workers that have seen the job as pending.
  • The chargedBy set records workers that commit a charge.
  • The Init predicate starts with an unclaimed job plus empty worker sets.
  • Save broken/JobProcessor.tla by pressing Cmd+S (macOS) or Ctrl+S (Windows).
  • Open Cursor's command search by pressing Cmd+Shift+P (macOS) or Ctrl+Shift+P (Windows).
  • Type TLA+: Parse module into the command search.
  • Select the matching command.

Cursor should report no syntax problems. This confirms that the module declaration plus its initial state are valid.

Seeing a Syntax Problem?

  • Confirm that the module name JobProcessor matches the file name JobProcessor.tla.
  • Check that the final line contains exactly four equals signs.
  • Help me fix the initial TLA+ module.
Separate observation from commitment

A nondeterministic interleaving can place another worker's action between a read and its later commit. The first action records which worker observed the unclaimed job.

  • Place your cursor directly above the closing ==== line in broken/JobProcessor.tla.
  • Paste the pending-read action using this code:
ReadPending(worker) ==
    /\ worker \in Workers
    /\ ~claimed
    /\ worker \notin observedPending
    /\ observedPending' = observedPending \cup {worker}
    /\ UNCHANGED <<claimed, chargedBy>>

How Does the Read Action Work?

  • The worker must belong to Workers.
  • The ~claimed guard permits the read while the job appears unclaimed.
  • The action adds that worker to observedPending.
  • The UNCHANGED expression preserves the claim status plus the charge record during this transition.
  • Save broken/JobProcessor.tla.
  • Return to Cursor's command search.
  • Run TLA+: Parse module again.

Cursor should report no syntax problems. The module now contains a valid action that caches a worker's pending observation.

Does the Read Action Fail to Parse?

  • Check that every conjunction uses the same operator shown in the code block.
  • Confirm that observedPending' ends with one apostrophe.
  • Help me debug the read action.

The second action trusts the cached observation in observedPending. It does not recheck the current value of claimed.

This creates the stale-read window that the model needs to represent. A worker can commit using information gathered in an earlier state.

  • Place your cursor below the ReadPending(worker) action.
  • Paste the charge action using this code:
CommitCharge(worker) ==
    /\ worker \in observedPending
    /\ worker \notin chargedBy
    /\ claimed' = TRUE
    /\ chargedBy' = chargedBy \cup {worker}
    /\ UNCHANGED observedPending

How Does the Commit Action Work?

  • The worker must have a cached observation in observedPending.
  • The worker must be absent from chargedBy.
  • The transition sets claimed to true.
  • The transition adds the worker to chargedBy.
  • The cached observations remain unchanged during the commit.
  • Save broken/JobProcessor.tla.
  • Return to Cursor's command search.
  • Run TLA+: Parse module again.

Cursor should report no syntax problems. Both halves of the racy transition boundary are now valid TLA+ actions.

Does the Commit Action Fail to Parse?

  • Confirm that claimed' ends with one apostrophe.
  • Confirm that chargedBy' ends with one apostrophe.
  • Check that UNCHANGED preserves observedPending.
  • Help me debug the commit action.
Complete and run the model

The Next relation gives TLC the actions it can choose from each state. The invariants separate valid data shapes from the at-most-once business promise.

  • Place your cursor below the CommitCharge(worker) action.
  • Paste the behavior plus both invariants above the closing ==== line using this code:
Next ==
    \/ \E worker \in Workers : ReadPending(worker)
    \/ \E worker \in Workers : CommitCharge(worker)

TypeOK ==
    /\ claimed \in BOOLEAN
    /\ observedPending \subseteq Workers
    /\ chargedBy \subseteq Workers

AtMostOnce ==
    Cardinality(chargedBy) \leq 1

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

What Completes the State Machine?

  • The Next relation lets TLC choose either action for either worker.
  • The TypeOK invariant checks that each variable retains its intended data shape.
  • The AtMostOnce safety invariant limits chargedBy to no more than one worker.
  • The Spec formula starts at Init.
  • The same formula allows repeated Next transitions.
  • Save broken/JobProcessor.tla.
  • Return to Cursor's command search.
  • Run TLA+: Parse module again.

Cursor should report no syntax problems. The complete racy state machine is ready for TLC.

Does the Completed Model Fail to Parse?

  • Confirm that the action names in Next match their definitions exactly.
  • Check that vars contains all three declared variables.
  • Confirm that Spec references vars.
  • Help me debug the completed specification.

A same-name configuration file tells TLC which behavior to explore. It also selects the properties that count as errors during this run.

  • In Cursor's file sidebar, select the broken directory.
  • Select the new-file control at the top of the file sidebar.
  • Name the file JobProcessor.cfg.
  • Paste the TLC configuration into broken/JobProcessor.cfg using this code:
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
INVARIANT TypeOK

What Does This Configuration Check?

  • The SPECIFICATION Spec line selects the temporal behavior from the module.
  • The CHECK_DEADLOCK FALSE line permits the model to reach its expected quiescent state.
  • The INVARIANT TypeOK line makes data-shape correctness the only enabled invariant.
  • The defined AtMostOnce invariant remains outside this run.
  • Save broken/JobProcessor.cfg.

Before you run the model, do you think valid state shapes are enough to stop both workers from charging?

  • Return to the terminal panel from the setup step.
  • Run the TypeOK-only model from the tla-job-processor folder using this command:
(cd broken && java -jar ../tools/tla2tools.jar JobProcessor.tla)

What Did TLC Prove?

You should see Model checking completed. No error has been found. TLC found no reachable state that violates TypeOK.

The run did not evaluate AtMostOnce because the configuration does not enable it. This result proves type correctness within the finite two-worker model.

That green baseline is an important milestone. Your runnable model now demonstrates how a successful check can leave the business promise unanswered.

Does TLC Fail to Complete?

  • Confirm that the terminal starts in the tla-job-processor folder.
  • Check that tools/tla2tools.jar remains inside the workspace.
  • Confirm that both files use the exact base name JobProcessor.
  • Help me troubleshoot the TLC run.

✔️ Awesome, I've got everything!

Your racy module passes its TypeOK-only model check. Save both files before moving on.

  • Save broken/JobProcessor.tla.
  • Save broken/JobProcessor.cfg.

ⓧ I'd like to double check the full code

Compare your two files with these complete references. The module defines AtMostOnce while the configuration enables only TypeOK.

---- MODULE JobProcessor ----
EXTENDS FiniteSets

Workers == {"worker-1", "worker-2"}

VARIABLES claimed, observedPending, chargedBy
vars == <<claimed, observedPending, chargedBy>>

Init ==
    /\ claimed = FALSE
    /\ observedPending = {}
    /\ chargedBy = {}

ReadPending(worker) ==
    /\ worker \in Workers
    /\ ~claimed
    /\ worker \notin observedPending
    /\ observedPending' = observedPending \cup {worker}
    /\ UNCHANGED <<claimed, chargedBy>>

CommitCharge(worker) ==
    /\ worker \in observedPending
    /\ worker \notin chargedBy
    /\ claimed' = TRUE
    /\ chargedBy' = chargedBy \cup {worker}
    /\ UNCHANGED observedPending

Next ==
    \/ \E worker \in Workers : ReadPending(worker)
    \/ \E worker \in Workers : CommitCharge(worker)

TypeOK ==
    /\ claimed \in BOOLEAN
    /\ observedPending \subseteq Workers
    /\ chargedBy \subseteq Workers

AtMostOnce ==
    Cardinality(chargedBy) \leq 1

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

====

What Should the Module Contain?

The complete module keeps observation separate from commitment. That boundary allows a worker to commit from a cached pending observation.

SPECIFICATION Spec
CHECK_DEADLOCK FALSE
INVARIANT TypeOK

What Should the Configuration Contain?

The configuration selects Spec while checking only TypeOK. This matches the intentionally incomplete baseline for this step.

Your racy processor now earns a green result from an intentionally incomplete check. Next, you will enable the business invariant and let TLC search for the harmful interleaving.

Expose the Double Charge

Your first TLC run proved that every reachable value had the expected shape. The duplicate-charge promise still had no check.

This step makes AtMostOnce part of the model check. A counterexample trace will reveal the harmful interleaving hidden by the earlier result.

In this step, get ready to:
  • Enable the at-most-once safety check in the broken model.
  • Run TLC to expose the duplicate charge.
  • Explain the stale-read failure shown by the numbered trace.
Enable the at-most-once invariant

A safety invariant describes something that must remain true in every reachable state. The existing AtMostOnce formula limits chargedBy to one worker.

  • In Cursor's file sidebar, select broken/JobProcessor.cfg.
  • Find this existing configuration:
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
INVARIANT TypeOK

What is checked right now?

The configuration tells TLC to evaluate Spec while checking TypeOK in every reachable state. The at-most-once promise is currently outside that check.

The deadlock setting keeps expected quiescence outside this exercise. The model can finish without TLC treating that stopped state as the target defect.

  • Add INVARIANT AtMostOnce directly below INVARIANT TypeOK so the file reads:
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
INVARIANT TypeOK
INVARIANT AtMostOnce

What changed?

The new line instructs TLC to evaluate AtMostOnce in every state it reaches. TypeOK remains enabled as a separate check.

The broken/JobProcessor.tla model stays unchanged. Only the promise being checked has expanded.

  • Save broken/JobProcessor.cfg.

✔️ Awesome, I've got everything!

Your saved configuration now checks both the model's data shapes and its at-most-once promise.

ⓧ I'd like to double check the full code

Compare your complete broken/JobProcessor.cfg file with this reference.

SPECIFICATION Spec
CHECK_DEADLOCK FALSE
INVARIANT TypeOK
INVARIANT AtMostOnce

What should the file contain?

This configuration keeps the original specification settings. It enables both TypeOK and AtMostOnce for the next model-checking run.

Run TLC to expose the violation

The model still separates reading the pending job from committing the charge. Checking the business invariant forces TLC to test whether that boundary permits a duplicate charge.

Before you run the check, do you expect the earlier green result to survive?

  • Run the broken model from the tla-job-processor folder by running this command:
(cd broken && java -jar ../tools/tla2tools.jar JobProcessor.tla)

What does this command check?

The subshell enters the broken folder for this run. TLC loads JobProcessor.tla with its same-name configuration file.

TLC explores the reachable states of the two-worker model. It evaluates both configured invariants during that search.

You'll see Error: Invariant AtMostOnce is violated. followed by a numbered state trace. This failure is the result you wanted.

TLC has found a reachable execution where chargedBy contains both workers. The earlier passing run hid this path because it checked only TypeOK.

Model still passes?

  • Confirm INVARIANT AtMostOnce appears in broken/JobProcessor.cfg.
  • Save broken/JobProcessor.cfg before rerunning the model.
  • Help me find why the broken model still passes.
Read the stale-read counterexample

Each numbered state is a snapshot of the variables after one transition. Reading the changing sets in order turns the formal trace into a concrete story about two workers racing.

  • Return to the terminal output from the TLC run.
  • Locate the initial state where claimed is FALSE.
  • Follow observedPending until it contains both workers.
  • Continue until chargedBy first contains one worker.
  • Read the final state where chargedBy contains both workers.

How does the duplicate charge happen?

  • Both ReadPending(worker) actions run while claimed is FALSE.
  • The observedPending set then contains both workers.
  • The first CommitCharge(worker) action sets claimed to TRUE.
  • That commit adds one worker to chargedBy.
  • The other observed worker still has an enabled CommitCharge(worker) action.
  • The second commit grows chargedBy to two workers. That violates AtMostOnce.

What has TLC proved?

This counterexample proves that the current TLA+ model permits a duplicate charge. It covers exactly the two workers named in Workers.

The result does not cover application code. It does not cover worker populations beyond worker-1 and worker-2.

Before you check the final state, which variable do you expect to show the broken promise?

  • Return to the final numbered state in the terminal output.
  • Confirm chargedBy contains worker-1 and worker-2.
  • Scan upward to confirm both ReadPending(worker) transitions occur before both CommitCharge(worker) transitions.

You can see both workers cache the pending observation before either charge commits. Two members in chargedBy make AtMostOnce false.

You have turned an informal race into a reproducible counterexample. Next, you will move the claim check and charge update into one atomic transition.

Make Claim and Charge Atomic

Your broken model has turned the stale-read race into a concrete counterexample. The numbered trace showed exactly where the at-most-once promise failed.

In the fixed TLA+ state machine, the claim check shares one transition with the charge update. TLC can examine every reachable state in the same two-worker scope.

In this step, get ready to:
  • Build the corrected TLA+ model with one atomic claim-and-charge action.
  • Configure TLC to check the type invariant and the at-most-once invariant.
  • Verify the repaired transition against the broken counterexample.
Build the atomic transition

An atomic action gives TLC one indivisible transition to evaluate. The ~claimed guard shares that transition with both state updates.

  • Return to Cursor from the previous step.
  • Select the fixed folder in the Explorer sidebar.
  • Use the file creation control at the top of the Explorer sidebar.
  • Enter JobProcessor.tla as the file name.
  • Press Enter to create the file.
  • Fill fixed/JobProcessor.tla by pasting this runnable base model:
---- MODULE JobProcessor ----
EXTENDS FiniteSets

Workers == {"worker-1", "worker-2"}

VARIABLES claimed, chargedBy
vars == <<claimed, chargedBy>>

Init ==
    /\ claimed = FALSE
    /\ chargedBy = {}

ClaimAndCharge(worker) ==
    /\ worker \in Workers
    /\ ~claimed
    /\ claimed' = TRUE
    /\ chargedBy' = chargedBy \cup {worker}

Next ==
    \E worker \in Workers : ClaimAndCharge(worker)

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

====

What Does This Model Establish?

  • The Workers set fixes the model's scope at two workers.
  • The claimed variable records whether the job has already been claimed.
  • The chargedBy set records which worker performed the charge.
  • The ClaimAndCharge(worker) action checks the claim before updating both variables in the same transition.
  • The Next action lets TLC choose either worker for the transition.
  • Save fixed/JobProcessor.tla.
  • Press Cmd+Shift+P (macOS) or Ctrl+Shift+P (Windows) to open the command palette.
  • Type TLA+: Parse module into the command palette.
  • Select TLA+: Parse module.

Good, the atomic transition now parses as one coherent state machine. The old cached observation has no place in this model.

Seeing a Parsing Problem?

  • Check that each state condition begins with /\.
  • Confirm that the closing ==== line remains at the bottom of the file.
  • Compare every apostrophe in claimed' and chargedBy' with the code block.
  • Help me diagnose my fixed TLA+ module parsing problem.

A type invariant checks the shape of every state. A safety invariant checks whether every state preserves the at-most-once promise.

  • Find the line that begins with Spec == in fixed/JobProcessor.tla.
  • Add both invariants directly above that line by pasting this code:
TypeOK ==
    /\ claimed \in BOOLEAN
    /\ chargedBy \subseteq Workers

AtMostOnce ==
    Cardinality(chargedBy) \leq 1

What Do These Invariants Check?

  • The TypeOK invariant requires claimed to remain Boolean.
  • The same invariant requires every member of chargedBy to come from Workers.
  • The AtMostOnce invariant limits chargedBy to one worker in every reachable state.
  • Save fixed/JobProcessor.tla.
  • Open the command palette with Cmd+Shift+P (macOS) or Ctrl+Shift+P (Windows).
  • Run TLA+: Parse module again.

Both invariant definitions now parse with the atomic transition. Your model is ready for TLC configuration.

Are the Invariants Failing to Parse?

  • Check that TypeOK and AtMostOnce appear above Spec.
  • Confirm that the subset operator is \subseteq.
  • Confirm that the cardinality comparison uses \leq.
  • Help me fix my TLA+ invariant syntax.
Configure the safety checks

The configuration file tells TLC which behavior to explore. It also names the invariants that TLC must evaluate in every reachable state.

  • Select the fixed folder in Cursor's Explorer sidebar.
  • Use the file creation control at the top of the Explorer sidebar.
  • Enter JobProcessor.cfg as the file name.
  • Press Enter to create the file.
  • Configure TLC by pasting these settings into fixed/JobProcessor.cfg.
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
INVARIANT TypeOK
INVARIANT AtMostOnce

What Does This Configuration Check?

  • The SPECIFICATION Spec line selects the model behavior defined in JobProcessor.tla.
  • The CHECK_DEADLOCK FALSE line keeps the check focused on safety invariants when the model reaches a quiescent state.
  • The two INVARIANT lines require TLC to check the state types and the at-most-once promise.
  • Save fixed/JobProcessor.cfg.
  • Confirm that Cursor's Explorer shows JobProcessor.tla and JobProcessor.cfg inside fixed.

Missing the Configuration File?

  • Check that JobProcessor.cfg sits inside fixed beside JobProcessor.tla.
  • Confirm that both files use the same JobProcessor base name.
  • Help me check my fixed model file layout.

✔️ Awesome, I've got everything!

  • Save fixed/JobProcessor.tla.
  • Save fixed/JobProcessor.cfg.

ⓧ I'd like to double check the full code

These are the complete fixed files at this point.

---- MODULE JobProcessor ----
EXTENDS FiniteSets

Workers == {"worker-1", "worker-2"}

VARIABLES claimed, chargedBy
vars == <<claimed, chargedBy>>

Init ==
    /\ claimed = FALSE
    /\ chargedBy = {}

ClaimAndCharge(worker) ==
    /\ worker \in Workers
    /\ ~claimed
    /\ claimed' = TRUE
    /\ chargedBy' = chargedBy \cup {worker}

Next ==
    \E worker \in Workers : ClaimAndCharge(worker)

TypeOK ==
    /\ claimed \in BOOLEAN
    /\ chargedBy \subseteq Workers

AtMostOnce ==
    Cardinality(chargedBy) \leq 1

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

====
SPECIFICATION Spec
CHECK_DEADLOCK FALSE
INVARIANT TypeOK
INVARIANT AtMostOnce
Verify the atomic repair

The broken model spreads one business operation across ReadPending(worker) and CommitCharge(worker). The fixed model expresses that operation through one transition named ClaimAndCharge(worker).

  • Display broken/JobProcessor.tla in one Cursor editor pane.
  • Display fixed/JobProcessor.tla beside it in a second editor pane.
  • Locate ReadPending(worker) in the broken model.
  • Locate CommitCharge(worker) in the broken model.
  • Locate ClaimAndCharge(worker) in the fixed model.
  • Trace where the ~claimed guard sits relative to the two assignments in each model.

In the fixed model, a worker that passes ~claimed performs both assignments within that transition. TLC evaluates the next action after claimed has become TRUE.

Before you run the fixed model, do you think TLC can reconstruct the double-charge trace from the broken model?

  • Return to the terminal you used for the broken model.
  • Run the fixed model from the tla-job-processor folder by using this command:
(cd fixed && java -jar ../tools/tla2tools.jar JobProcessor.tla)

What Does This Check Run?

  • The command temporarily runs inside the fixed folder.
  • Java starts TLC from ../tools/tla2tools.jar.
  • TLC loads JobProcessor.tla with its same-name JobProcessor.cfg configuration.
  • The configuration asks TLC to evaluate both TypeOK and AtMostOnce.

That is the atomic repair verified. You should see Model checking completed. No error has been found. in the terminal output.

TLC Did Not Complete Cleanly?

  • Confirm that your terminal starts in the tla-job-processor folder.
  • Check that fixed/JobProcessor.tla matches the complete model in the double-check tab.
  • Check that fixed/JobProcessor.cfg enables both invariants.
  • Help me troubleshoot my fixed TLC run.

You now have the broken counterexample beside its atomic repair. The transition boundary makes the difference visible in code.

What Has TLC Proved?

This is a bounded model checking result over the literal two-worker set. Every reachable state in that finite model satisfies TypeOK and AtMostOnce.

Application code sits outside this model. Larger worker populations require their own modeled scope.

Secret mission

Prove Completion Requires a Charge

Extend the fixed processor with a completion state and a guarded finish transition. Then use TLC to verify that every completed job has exactly one recorded charge within the finite two-worker model.

Clean Up Your Resources

Clean Up Your Resources

Everything in this project runs locally. There are no ongoing costs or cloud resources to remove.

Decide whether to keep your model files available, close Cursor for now, or delete the local demo entirely.

Resources you used:

  • The tla-job-processor folder stores broken/, fixed/, plus the pinned TLC JAR at tools/tla2tools.jar.
  • The TLA+ (Temporal Logic of Actions) extension installed in Cursor.

Keep everything running

No action is needed. Choose this option if you want to rerun the counterexample or extend the fixed model.

  • Keep tla-job-processor on your Mac as a side-by-side formal verification demo.
  • Leave the TLA+ extension installed in Cursor for future models.
  • Leave Microsoft Build of OpenJDK 21 installed for other local tools.

Pause - I'll come back to this later

Pausing only means closing the editor. No TLC process or service continues after a completed run.

  • Close the Cursor window.
  • Keep tla-job-processor on disk for your return.

Delete - I don't want to use this again

Deletion removes the project-specific resources from your Mac. The folder remains recoverable from Trash until you empty it.

  • In Cursor, select the Extensions icon in the Activity Bar.
  • Search for TLA+ (Temporal Logic of Actions).
  • Select the TLA+ (Temporal Logic of Actions) extension.
  • Click Uninstall.
  • In Finder, locate the tla-job-processor folder.
  • Move tla-job-processor to Trash.
  • Empty Trash to remove the folder permanently.

You should no longer see the tla-job-processor folder in Finder. The TLA+ extension should no longer appear among the installed extensions in Cursor.

Microsoft Build of OpenJDK 21 remains installed for other local tools.

Nice Work!

Nice Work!

Excellent work! You built side-by-side TLA+ models that preserve the unsafe processor beside its corrected version.

You've learned how to:

  • Built finite state machines for two workers racing to claim one job.
  • Used a TLC counterexample trace to reveal both workers acting on stale pending observations. This showed why TypeOK could pass while AtMostOnce failed.
  • Moved the claim check plus charge update into one atomic transition. Verified TypeOK and AtMostOnce across every reachable state in the finite two-worker model.
  • Secret Mission: Added the Finish transition plus the CompletionRequiresCharge safety invariant. The bounded check confirmed that every completed state contains exactly one charge.

Ready to quiz yourself?