anmandu

My notes on Fighting Complexity: Formal Methods, Resilient Runtimes, and the New AI Harness

Software does not usually fail because someone wrote a bad for loop. It fails because nobody could hold the whole system in their head anymore. Complexity is the actual adversary, and most of our tooling treats it as a fact of life rather than a problem to be attacked.

These are notes on the engineers who refused to accept that — and on the tools they built to fight back.

1. The problem: complexity and chaos

Modern software carries an inherent instability that comes from unpredictable engineering design. The classic essay on this is Out of the Tar Pit (Ben Moseley and Peter Marks, 2006), and its diagnosis is uncomfortable because it is correct: the largest source of complexity in real systems is state and control flow.

Not the domain. Not the algorithms. State — the mutable, sprawling, hard-to-reason-about kind — plus the tangle of when things happen. The paper separates essential complexity (inherent to the problem you are solving) from accidental complexity (everything we pile on top by accident), and argues that most of what drowns us is accidental.

Their proposed exit is functional programming and the relational model — minimize mutable state, declare data relationships instead of orchestrating them by hand.

This is the foundation everything else in this post is built on. If you skip it, the rest reads like academic decoration. It isn't.

2. The solution: formal methods and verification

If you want systems that do not get it wrong, at some point testing stops being enough. Tests sample the space of possible behaviors. Formal methods reason about all of it.

This is not theory sitting in a drawer. AWS runs on it.

TLA+

TLA+ is a specification language created by Leslie Lamport for modeling systems — especially distributed ones — and checking their properties before a line of code exists.

The value is that it finds design errors, the class of bug traditional testing structurally cannot reach: the race that only appears when three nodes fail in a specific order, the invariant that holds in every test you thought to write and breaks on the one you didn't.

AWS documented this publicly in How Amazon Web Services Uses Formal Methods (CACM, 2015). Read it as evidence, not as a manifesto: they used it on S3, DynamoDB, and EBS, and found real defects.

Tooling worth knowing: the TLA+ Toolbox, the TLC model checker, and PlusCal if the algorithmic notation is easier to start with.

Cedar

Cedar is an authorization policy language designed from the start to be fast, safe, and analyzable by automated reasoning.

That last property is the interesting one. Most authorization logic ends up as scattered if statements nobody can audit as a whole. Cedar makes policies first-class artifacts you can ask questions about — "can this policy ever grant access to X?" — and get an answer from a solver rather than from a hopeful code review.

Source: github.com/cedar-policy/cedar. It backs Amazon Verified Permissions.

Lean 4

Lean 4 is a proof assistant and programming language used to mechanically verify that a system and its invariants are correct.

"Mechanically" is the operative word. A proof in Lean is checked by a machine, not accepted because a smart person nodded at it. That is a categorically different guarantee than a test suite passing.

If you want to see how far this goes, mathlib is a formalization of a substantial chunk of modern mathematics in Lean.

3. High-availability runtimes

Design correctness is half the story. The other half is what happens at 3 a.m. when a dependency starts timing out.

Erlang/OTP

Erlang/OTP came out of telecom, where "the system is down" is not an acceptable sentence. Its philosophy was formalized in Joe Armstrong's thesis, Making Reliable Distributed Systems in the Presence of Software Errors (2003), and it inverts the instinct most developers have:

Let it crash.

Do not write defensive code trying to handle every failure inline. Let the failing process die cleanly, isolate the damage, and let a supervisor restart it into a known-good state. You stop pretending you can enumerate every failure mode, and instead you make recovery cheap and automatic.

This rests on the actor model: lightweight processes that share nothing and communicate only by message passing. No shared mutable state means no shared corruption — which is the same lesson Out of the Tar Pit was teaching, arriving from a completely different direction.

OTP is the framework of battle-tested patterns — supervision trees, gen_server, and friends — that turn that philosophy into something you can actually ship.

BEAM

BEAM is the virtual machine underneath. It is built for total process isolation and low latency: preemptive scheduling, per-process heaps, and garbage collection that does not stop the world.

That is why a BEAM system degrades gracefully instead of falling over — one misbehaving process cannot monopolize the scheduler or freeze everyone else. Elixir and Phoenix are the most common modern doors into this runtime.

4. AI and knowledge management

The same discipline is now being applied to the AI stack. The new harness for enterprise AI:

CoALA

CoALA — Cognitive Architectures for Language Agents — proposes a structured framework for how language agents organize memory and action, drawing on decades of prior work in cognitive architectures.

It separates working memory from long-term memory (episodic, semantic, procedural) and defines a decision loop over internal and external actions. If you have been building agents by piling prompts on top of prompts, this is the architectural vocabulary you have been missing.

vLLM

vLLM solves the unglamorous problem that decides whether your LLM feature is affordable: memory management at serving time.

Its core contribution is PagedAttention, which applies the idea of virtual memory paging to the attention KV cache. Instead of reserving one contiguous block per sequence and wasting most of it, it allocates in pages. The result is dramatically higher throughput on the same hardware.

Note what happened there: a decades-old operating systems concept, correctly applied to a new domain. Fundamentals do not expire.

TypeQL

TypeQL is a query language grounded in type theory, built for polymorphic knowledge databases. It is the query surface of TypeDB.

The pitch: model your domain with inheritance, interfaces, and n-ary relations directly, and let the engine do rule-based inference over it — rather than flattening everything into join tables and reconstructing meaning in application code.

The thread running through all of this

None of these tools are the point. The pattern is:

  • Out of the Tar Pit — attack complexity at its source: state.
  • TLA+, Cedar, Lean — replace hope with proof.
  • Erlang/OTP, BEAM — assume failure, and make recovery structural.
  • CoALA, vLLM, TypeQL — apply that same rigor to the AI stack instead of improvising.

Every one of them is someone deciding that "it usually works" is not a good enough answer.

That is the whole discipline. The tools change every five years. That standard doesn't.

References