TLA+ Chaos Loop

Automated formal verification pipeline: Source Code → AST Detection → TLA+ Model → TLC Counter-Example → Chaos Confirmation → Fix → Re-verify

The Problem

Writing TLA+ specifications requires expertise most engineers don't have. Even when models exist, there's no systematic way to confirm that a TLC counter-example corresponds to a real failure in production code.

The Solution

TLA+ Chaos Loop automates the entire cycle. The key insight: most concurrency bugs follow a small set of detectable antipatterns. By cataloging these patterns, we can automate detection → formalization → verification → confirmation.

Quick Start

# Install dependencies
npm install

# Run the full pipeline on your codebase
npx tsx src/cli.ts <target-directory> --formalize --verify --chaos

# Example: run on the test fixtures
npx tsx src/cli.ts src/__tests__/ --formalize --verify

CLI Flags

| Flag | Description | |------|-------------| | --formalize / -f | Generate TLA+ micro-specs from detected patterns | | --verify / -c | Run TLC model checker on generated specs | | --chaos / -c | Run chaos engineering confirmation (requires Toxiproxy) | | --llm / -L | Use LLM for formalization (requires API key) | | --pluscal / -P | Use PlusCal format for LLM generation | | --iterative / -I | Iterative LLM correction (TLC-guided retry) | | --auto-correct / -A | Fast SANY syntax check before human review | | --review / -R | Human-in-the-loop review before TLC |

Verified Core

Patterns with full pipeline: AST detection → TLA+ model → TLC counter-example → chaos confirmation.

| Pattern | Languages | TLC Violation | Chaos Method | |---------|-----------|---------------|--------------| | SYNC_IO_IN_LOCK | JS, Java, Go | Invariant: NoSyncIOInCriticalSection | Latency injection (5s) | | MISSING_ERROR_HANDLING | JS | Temporal: EventuallyResolved | Timeout (100ms) | | UNGUARDED_SHARED_STATE | JS | Invariant: StateMutatedUnderLock | Packet slicing | | RACE_CONDITION | JS | Invariant: NoLostUpdate | Packet slicing | | DEADLOCK_RISK | Go | Invariant: NoDeadlock | Asymmetric latency | | TIMEOUT_VIOLATION | Go | Invariant: TimeoutDetected | Extreme latency (10s) |

Case Study: NATS Server

Full pipeline on NATS Server (Go, 800K+ LOC):

Total findings:     2,516
Critical:           505 (25.1%)  — SYNC_IO_IN_LOCK, DEADLOCK_RISK
High:             1,555 (61.8%)  — TIMEOUT_VIOLATION, SYNCHRONOUS_POISON
Medium:             456 (18.1%)  — MISSING_ERROR_HANDLING, LEGACY_STREAMING_API

Deadlock risks:     493 functions with multiple locks
Timeout violations: 540 functions with unchecked timeouts
Sync I/O in lock:   12 instances in filestore.go

Project Structure

tla-chaos-loop/
├── docs/                    # Methodology and pipeline description
│   ├── architecture.md      # Pipeline architecture and component details
│   ├── methodology.md       # Verification methodology and categories
│   └── article.md           # Full paper (543 lines)
├── sensors/                 # Sensor plugin documentation
│   └── README.md            # Language support matrix and sensor details
├── specs/                   # TLA+ model library (hand-verified)
│   ├── sync_io_in_lock.tla
│   ├── missing_error_handling.tla
│   ├── unguarded_shared_state.tla
│   ├── race_condition.tla
│   ├── deadlock_risk.tla
│   └── timeout_violation.tla
├── chaos/                   # Toxiproxy scripts and configs
│   ├── toxiproxy-setup.sh   # Bash setup script
│   └── scenarios.json       # Machine-readable configs
├── examples/                # Step-by-step PoC walkthroughs
│   ├── sync_io_in_lock.md
│   ├── deadlock_risk.md
│   └── timeout_violation.md
└── src/                     # TypeScript implementation
    ├── sensors/             # AST sensor, NATS sensor, trace sensor
    ├── detection/           # Rule engine for warning classification
    ├── formalization/       # TLA+ generation (templates, renderer, TLC runner, PlusCal utils)
    ├── chaos/               # Toxiproxy client, scenarios, feedback loop
    ├── __tests__/           # Unit + integration tests (86 tests)
    └── cli.ts               # Pipeline entry point

Requirements

• Node.js 20+
• Java (for TLC model checker)
• Toxiproxy (for chaos engineering — optional)
• tools/tla2tools.jar (TLC — included in repo)

Architecture

┌─────────────────────────────────────────────────────────────┐
│                    Source Code                               │
└─────────────────────┬───────────────────────────────────────┘
                      │
                      ▼
┌─────────────────────────────────────────────────────────────┐
│  Layer 1: Detection (AST Sensor)                            │
│  web-tree-sitter WASM • JS, Java, Go, PHP, Python           │
│  Structural analysis: lock+I/O, error handling, races       │
└─────────────────────┬───────────────────────────────────────┘
                      │ SensorFinding[]
                      ▼
┌─────────────────────────────────────────────────────────────┐
│  Layer 2: Formalization (TLA+ Generator)                    │
│  Template → MicroSpec → renderTla()                         │
│  OR: LLM → PlusCal → pcal.Translator → TLA+                │
└─────────────────────┬───────────────────────────────────────┘
                      │ .tla + .cfg files
                      ▼
┌─────────────────────────────────────────────────────────────┐
│  Layer 3: Verification (TLC Model Checker)                  │
│  Exhaustive state exploration • Counter-example traces      │
└─────────────────────┬───────────────────────────────────────┘
                      │ Violation report
                      ▼
┌─────────────────────────────────────────────────────────────┐
│  Layer 4: Confirmation (Chaos Engineering)                  │
│  Toxiproxy fault injection • Empirical validation          │
└─────────────────────┬───────────────────────────────────────┘
                      │
                      ▼
┌─────────────────────────────────────────────────────────────┐
│  Fix → Re-verify (close the loop)                           │
└─────────────────────────────────────────────────────────────┘

How It Works

1. Detection: AST sensor walks parse trees structurally — finds lock acquisition nodes, then checks following siblings for I/O calls, promise chains without error handling, or read-modify-write sequences.

2. Formalization: Each antipattern maps to a TLA+ template. Templates define variables (locks, I/O state, operation progress), actions (transitions), and invariants (safety properties). Alternatively, LLM generates PlusCal code that pcal compiles to TLA+.

3. Verification: TLC exhaustively explores the state space. When it finds a counter-example, we parse the trace to identify which invariant was violated and the exact sequence of actions.

4. Confirmation: Chaos layer maps TLC violations to Toxiproxy fault injection. This closes the loop: the formal model predicts a failure, and chaos engineering reproduces it.

Tests

# Run all tests (unit + integration)
npm test

# Run specific test suite
npx vitest run src/__tests__/ast-sensor.test.ts
npx vitest run src/__tests__/pipeline.integration.test.ts
npx vitest run src/__tests__/pluscal-utils.test.ts

86 tests covering:

• AST detection for JS, Java, Go
• TLA+ generation and rendering
• TLC integration (counter-example detection)
• Full pipeline integration (AST → TLA+ → TLC)
• PlusCal normalization and invariant extraction
• Iterative formalization and feedback loop

Contributing

See docs/methodology.md for the verification methodology. Patterns must complete the full pipeline (detection → formalization → verification → confirmation) to be added to the Verified Core.

License

MIT