Temporal Logic of Actions (TLA+) Demo

A practical introduction to formal verification using TLA+ through a file upload idempotency problem.

What is TLA+?

TLA+ (Temporal Logic of Actions) is a formal specification language for modeling and verifying concurrent and distributed systems. It helps you:

• Model system behavior precisely using mathematical logic
• Find bugs before implementation through exhaustive state exploration
• Verify correctness properties like safety and liveness
• Document assumptions and invariants clearly

TLA+ is particularly powerful for systems where race conditions, edge cases, and complex state interactions can cause subtle bugs.

The Problem: Upload Idempotency

This demo models a common issue: ensuring file uploads are idempotent (safe to retry). We compare two approaches:

1. Buggy: Random UUID keys → duplicates on retry
2. Fixed: Content-addressed keys → idempotent uploads

Project Structure

├── specs/
│   ├── Uploads_bug.tla      # Models the buggy approach
│   ├── Uploads_bug.cfg      # Configuration for model checking
│   ├── Uploads_fixed.tla    # Models the fixed approach
│   ├── Uploads_fixed.cfg    # Configuration for fixed version
│   └── states/              # TLA+ model checker output
├── api/
│   ├── app.py              # FastAPI implementation (both versions)
│   ├── dockerfile          # Container for the API
│   └── requirements.txt    # Python dependencies
└── docker-compose.yml     # Local test environment

Installing TLA+

Option 1: VS Code Extension (Recommended)

1. Install VS Code
2. Install the TLA+ extension
3. The extension includes TLC model checker and PlusCal translator

Option 2: Standalone TLA+ Toolbox

1. Download from TLA+ official site
2. Extract and run the toolbox application
3. Import specifications as new projects

Option 3: Command Line (Linux/macOS)

# Install Java 8+ first
sudo apt install openjdk-11-jdk  # Ubuntu/Debian
brew install openjdk@11          # macOS

# Download TLA+ tools
wget https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar

# Run model checker
java -cp tla2tools.jar tlc2.TLC Uploads_bug.tla

Understanding the Examples

Buggy Version (Uploads_bug.tla)

The Problem:

RetrySame ==
  \E c \in Contents, k1, k2 \in Keys :
    /\ k1 # k2                                    \* Different keys
    /\ [content |-> c, key |-> k1] \in objects   \* Same content exists
    /\ objects' = objects \cup {[content |-> c, key |-> k2]}  \* Add duplicate

Invariant (should hold but doesn't):

AtMostOneKeyPerContent ==
  \A o1, o2 \in objects : o1.content = o2.content => o1.key = o2.key

Result: TLA+ finds a counterexample showing the invariant violation.

Fixed Version (Uploads_fixed.tla)

The Solution:

UploadDet ==
  \E c \in Contents :
    /\ objects' = objects \cup {[content |-> c, key |-> c]}  \* Key = content

Result: TLA+ verifies the invariant always holds.

Running the Verification

Check the Buggy Version

cd specs/
# Using VS Code: Open Uploads_bug.tla and run "TLA+: Check model with TLC"
# Or command line:
java -cp tla2tools.jar tlc2.TLC -config Uploads_bug.cfg Uploads_bug.tla

Expected output: Invariant violation found in 2-3 states.

Check the Fixed Version

# Using VS Code: Open Uploads_fixed.tla and run "TLA+: Check model with TLC"
# Or command line:
java -cp tla2tools.jar tlc2.TLC -config Uploads_fixed.cfg Uploads_fixed.tla

Expected output: No errors found, invariant holds.

Running the Implementation

Test the real FastAPI implementation that mirrors the TLA+ models:

# Start MinIO and API
docker-compose up

# Test buggy endpoint (creates duplicates)
curl -X POST -F "file=@somefile.txt" http://localhost:8000/upload_buggy
curl -X POST -F "file=@somefile.txt" http://localhost:8000/upload_buggy  # Different key!

# Test fixed endpoint (idempotent)
curl -X POST -F "file=@somefile.txt" http://localhost:8000/upload_hashed
curl -X POST -F "file=@somefile.txt" http://localhost:8000/upload_hashed  # Same key

Key TLA+ Concepts Demonstrated

• State space exploration: TLA+ checks all possible execution paths
• Invariants: Properties that should always hold (AtMostOneKeyPerContent)
• Actions: State transitions (UploadNew, RetrySame, UploadDet)
• Specifications: Complete system behavior (Spec == Init /\ [][Next]_vars)
• Model checking: Automated verification with concrete constants

Verification Results

We tested both approaches using formal verification:

Approach	Result	Verdict
Buggy Version (random UUIDs)	❌ FAILED	Invariant violated - creates duplicates
Fixed Version (content hashing)	✅ PASSED	All properties verified - idempotent uploads

🔍 What TLA+ Found in the Buggy Version

TLA+ discovered this exact sequence that breaks the system:

1. Step 1: System starts empty → Storage: {}
2. Step 2: Upload content "c1" with key "k1" → Storage: {[content: c1, key: k1]}
3. Step 3: Upload SAME content "c1" again, get different key "k2" → Storage: {[content: c1, key: k1], [content: c1, key: k2]}

Result: Same content now has two different keys, violating our core requirement.

✅ What TLA+ Verified in the Fixed Version

TLA+ mathematically proved that content-based hashing works:

1. Step 1: System starts empty → Storage: {}
2. Step 2: Upload content "c1", key becomes "c1" → Storage: {[content: c1, key: c1]}
3. Any retry: Upload "c1" again, still gets key "c1" → Storage: {[content: c1, key: c1]} (unchanged!)

Result: Same content always gets the same key - retries are completely safe.

📊 Impact Summary

Metric	Buggy Approach	Fixed Approach
Idempotency	❌ Not guaranteed	✅ Guaranteed
Storage efficiency	❌ Creates duplicates	✅ No duplicates
Retry safety	❌ Unsafe	✅ Completely safe
Predictability	❌ Random keys	✅ Deterministic keys

Why This Matters

This example demonstrates how TLA+ can:

1. Catch design flaws before coding (found the UUID bug in 896ms)
2. Prove correctness of the fix (mathematical verification)
3. Document precise behavior for implementation
4. Build confidence in system properties (100% coverage of state space)

TLA+ found a critical flaw that could cause wasted storage costs, production bugs, and poor user experience - all discovered at design time, not in production.

For real systems, TLA+ has found critical bugs in distributed databases, consensus protocols, and cloud services that would be nearly impossible to catch through testing alone.

Next Steps

• Read Leslie Lamport's TLA+ home page
• Try Learn TLA+ interactive tutorial
• Explore TLA+ examples repository