> ## 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.

# Formal Methods

> Mathematical specifications that prove models of systems work correctly.

Testing shows the presence of bugs, not their absence. You can run a million tests and still miss the race condition that crashes production at 2 AM. Formal methods offer a different approach, mathematical proof that certain bugs *cannot* exist.

This is not about replacing testing. It is about catching what testing misses such as race conditions, distributed system failures, permission gaps, and edge cases you did not think to check.

Formal methods find them by exploring *every possible* sequence of events.

<Info>
  AWS used TLA+ to find subtle bugs in S3, DynamoDB, and other core services. These bugs would never have been found through testing, and could have caused data loss in production.
</Info>

## How Formal Verification Works

You write a *model*, a mathematical abstraction of your system. The model captures the essential behavior you care about while ignoring irrelevant details. A model checker then exhaustively explores every possible state of this model, checking your properties against each one.

This is fundamentally different from testing. Testing checks specific scenarios you thought to write. Model checking explores the entire state space. AWS found a [35-step bug in DynamoDB](https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf) that escaped all their tests and two code reviews. The model checker found it because it explored paths no human thought to test.

<Warning>
  Formal methods verify the model, not the code. The guarantee is only as good as the model's fidelity to the real system.
</Warning>

### The Model Must Be Accurate

When a model checker reports "no violations found," it means the properties hold *in your model*. If your model accurately represents the real system, you gain confidence. If your model diverges from reality, bugs can hide in the gap.

A [2016 study by Fonseca et al.](https://blog.acolyer.org/2017/05/29/an-empirical-study-on-the-correctness-of-formally-verified-distributed-systems/) examined three formally verified distributed systems: Iron Fleet, Verdi, and Chapar. They found 16 bugs through testing and code review. The results were instructive:

* **Zero protocol-level bugs.** The verification worked. The core distributed algorithms were correct.
* **11 bugs in the shim layer.** The interface between verified and unverified code, where assumptions about the operating system and network were encoded, contained most issues.

The lesson: verification improves confidence, not perfection. Document your assumptions. Pay extra attention to interface code. Consider conformance testing, where you generate test cases from your specifications to verify the implementation matches the model.

### Abstraction Is a Tradeoff

Abstraction makes verification tractable. Real systems have infinite or astronomically large state spaces. By abstracting away details, we reduce the state space to something a model checker can explore.

The [seL4 microkernel](https://sel4.systems/Info/FAQ/proof.pml), among the most thoroughly verified software ever created, explicitly [documents what it assumes](https://sel4.systems/Verification/assumptions.html): assembly code correctness, boot code behavior, hardware functioning per specification, and more.

This honestly is brilliant.

The verification is real and valuable. But the team explicitly delineates where the proof ends and trust begins.

## Learning Paths

Two complementary approaches, each with a learning progression from basics to real-world application.

### TLA+

TLA+ models systems as state machines and verifies temporal properties: what happens over sequences of operations.

<CardGroup cols={2}>
  <Card title="TLA+ Basics" icon="graduation-cap" href="/formal-methods/tla-basics">
    Gentle introduction for beginners. Build a light switch, then find a concurrency bug in a bank transfer system.
  </Card>

  <Card title="TLA+ Syntax Guide" icon="book" href="/formal-methods/tla-syntax-guide">
    Complete language reference. Set theory, operators, temporal logic, and common patterns.
  </Card>
</CardGroup>

### Alloy

Alloy analyzes structural properties and finds counterexamples: specific configurations that violate your assertions. Alloy 6 added temporal operators, enabling behavioral verification similar to TLA+.

<CardGroup cols={2}>
  <Card title="Alloy Basics" icon="graduation-cap" href="/formal-methods/alloy-basics">
    Gentle introduction for beginners. Model a file system, then discover a permission bug when files move between folders.
  </Card>

  <Card title="Alloy Syntax Guide" icon="book" href="/formal-methods/alloy-syntax-guide">
    Complete language reference including Alloy 6 temporal features, relational operators, and common patterns.
  </Card>
</CardGroup>

## When to Use Which

| Aspect           | TLA+                                          | Alloy                                              |
| ---------------- | --------------------------------------------- | -------------------------------------------------- |
| **Focus**        | Behavior over time                            | Structure (temporal in Alloy 6+)                   |
| **Question**     | "Does this sequence of operations stay safe?" | "Can this bad configuration exist?"                |
| **Verification** | Model checking (exhaustive state exploration) | SAT solving (constraint satisfaction)              |
| **Strength**     | Protocols, concurrency, distributed systems   | Data models, permissions, access control           |
| **Output**       | Counterexample traces (sequences of states)   | Counterexample instances (specific configurations) |

**Use TLA+ when** you care about sequences: distributed consensus, concurrent data structures, transaction protocols. The [TLA+ Basics](/formal-methods/tla-basics) guide demonstrates this by finding a bug where concurrent bank transfers cause negative balances, something unit tests would miss.

**Use Alloy when** you care about structure: permission models, data schemas, network topologies. The [Alloy Basics](/formal-methods/alloy-basics) guide demonstrates this by finding a bug where moving a file between folders accidentally revokes access, a counterexample Alloy finds automatically.

<Tip>
  Many real systems benefit from both. Use TLA+ for the protocol logic, Alloy for the data model. They verify different properties.
</Tip>

## Native macOS Tools

Running formal verification traditionally requires Java-based tools. I built native macOS alternatives that run locally:

<CardGroup cols={2}>
  <Card title="MacTLA" icon="apple" href="/formal-methods/mactla">
    Native TLA+ IDE with built-in model checking, PlusCal translation, and interactive state visualization.
  </Card>

  <Card title="MacAlloy" icon="apple" href="/formal-methods/macalloy">
    Native Alloy 6.2 IDE with built-in CDCL SAT solver and force-directed instance visualization.
  </Card>
</CardGroup>

No JVM required. No AI integration, it's a simple set of Mac native applications

## Domain Applications

Formal methods applied to specific domains, from security to safety-critical systems.

### Active Directory Security

Verify that AD tier models prevent credential theft and privilege escalation. Mathematically prove no attack paths exist.

<CardGroup cols={2}>
  <Card title="AD TLA+ Specification" icon="clock" href="/formal-methods/tla-specification">
    Example specification reviewing Active Directory, temporal verification of tier isolation. 10 safety invariants covering credential protection and state transitions.
  </Card>

  <Card title="AD Alloy Specification" icon="shield-halved" href="/formal-methods/alloy-specification">
    Example specification reviewing Active Directory, for structural analysis of ACLs for attack paths. 11 predicates covering DCSync, RBCD abuse, Shadow Credentials, and more.
  </Card>
</CardGroup>

### Binary Analysis

Formal methods for reverse engineering and vulnerability research. Constraint solving meets binary analysis.

<Card title="Formal Methods for Binary Analysis" icon="microchip" href="/formal-methods/formal-methods-binary-part1">
  Three-part series covering SAT/SMT solvers, symbolic execution, and practical applications in malware analysis and exploit development.
</Card>

## Getting Started

**New to formal methods?** Start with [TLA+ Basics](/formal-methods/tla-basics) or [Alloy Basics](/formal-methods/alloy-basics). They assume no prior knowledge and build intuition through progressive examples.

**Ready to write specifications?** Use the syntax guides as reference while working on your own models.

**Have a specific domain?** Jump directly to the domain applications. They show formal methods applied to real problems.

**On macOS?** Download [MacTLA](/formal-methods/mactla) or [MacAlloy](/formal-methods/macalloy) for the fastest path from specification to verification.