Modeling Apache Redirect Rules in TLA+

An .htaccess file is a program. Each RewriteRule and Redirect directive is a transition in a state machine where the state is a URL and the transitions are rewrites. When rules interact – one rule's output is another rule's input – the composition can loop.

The wal.sh .htaccess has grown to include:

• HTTPS enforcement (http → https)
• Canonical URL enforcement (.html → extensionless, 301)
• Ghost page removal (README.html → 410)
• Content negotiation (extensionless → .md when Accept: text/markdown)
• Extensionless fallback (extensionless → .html, internal rewrite)
• Legacy path redirects (encode → transform, graphql/* → *, etc.)
• Explicit per-page redirects (flat file → directory, etc.)

The dangerous interaction is between rules 2 and 5:

Rule 2: /research/apl.html → /research/apl  (301 external)
Rule 5: /research/apl     → /research/apl.html  (internal rewrite)

On paper, this loops. In practice, Apache's THE_REQUEST variable – which freezes the original client request and never changes on internal rewrites – prevents rule 2 from re-firing. But "in practice" is not a proof. The question is whether this holds across all URL permutations: with query params, with trailing slashes, with README.html fragments, with the Accept header varying, with the legacy redirects interleaving.

That question is a model-checking question.

You could curl every URL. We have ~682 pages, 2 schemes, 2 extensions, an Accept header toggle, and query params – call it 5,000 test cases. But:

1. You only test the URLs that exist today. A future page at a new path might hit a rule interaction you never tested.
2. Redirect chains are sequential – a 3-hop chain means 3 HTTP requests. At scale, this is slow and flaky.
3. The interesting bugs are in the rule interaction, not the individual rules. Testing individual URLs does not prove the absence of loops in the composition.

TLA+ explores the state space exhaustively. The model has a finite set of URL shapes, a finite set of rules, and a bounded hop count. The model checker (TLC) enumerates every reachable state and verifies two properties:

• Safety: hops < MaxHops= – no redirect storm.
• Liveness: <>(phase = "done") – every request eventually terminates.

If either property fails, TLC produces a counterexample: the exact sequence of rule firings that violates the property. That counterexample is the bug.

The full spec is at docs/htaccess-redirect-spec.tla. The key design decisions:

Before modeling, the .htaccess contained:

Redirect 301 /research/local-first/ /research/local-first.html

This redirects a trailing-slash request to the .html file. Combined with the new global .html → extensionless rule, the chain becomes:

GET /research/local-first/
  → 301 /research/local-first.html    (explicit Redirect, line 142)
  → 301 /research/local-first         (global .html→extensionless rule)
  → internal rewrite to local-first.html
  → 200

Three hops instead of one. Not a loop, but a wasteful chain. The TLA+ model flagged this as a state with hops = 2 before reaching done. The fix: redirect directly to the extensionless canonical:

Redirect 301 /research/local-first/ /research/local-first

Now: one hop, then internal rewrite, then 200.

The ?w= and ?t= query parameters are Winding Web Ring (WWN) torus coordinates. They generate an infinite URL space by design – a honeypot that traps aggressive crawlers in an endless traversal. Amazonbot's 28K requests/day on these coordinates is the trap working.

The TLA+ model explicitly excludes these parameters from redirect rules. The invariant is:

Query params ?w= and ?t= MUST pass through all redirect rules unchanged.
No rule may strip, rewrite, or redirect based on w or t values.

This is a safety property of the redirect system, not a liveness property. The webring's non-termination is in the crawl graph, not in the redirect chain. Any single request with ?w=3&t=1 terminates in one hop (200). The non-termination is that following the links on the served page leads to ?w=4&t=1, then ?w=5&t=1, forever. That is the webring, not a redirect loop.

The .htaccess header now mandates:

Any change to redirect or rewrite rules MUST be modeled in TLA+
before deployment to prove termination across all URL permutations.

In practice:

1. Edit docs/htaccess-redirect-spec.tla to add the new rule as a transition.
2. Run TLC: tlc HtaccessRedirects -config HtaccessRedirects.cfg
3. If TLC finds a counterexample, the rule interaction is unsafe. Fix it.
4. If TLC passes, the composition terminates. Deploy.

The initial state space is small (~5,000 states for 6 paths × 2 schemes × 2 extensions × 2 accepts × 2 query shapes × 2 fragments). TLC explores it in under a second. Adding a new redirect rule adds one transition and marginally increases the state space. The cost of running the check is negligible compared to debugging a redirect storm in production.

The .htaccess includes intentional non-terminating redirects under /ouroboros/. The bare path /ouroboros redirects here (to this page). The sub-paths are the test canaries:

When you run the TLA+ model checker with /ouroboros/a in the initial state, TLC must report a liveness violation:

Error: Temporal properties were violated.
The following behavior constitutes a counterexample:
  State 1: request.path = "ouroboros/a", phase = "redirect", hops = 0
  State 2: request.path = "ouroboros/b", phase = "redirect", hops = 1
  State 3: request.path = "ouroboros/a", phase = "redirect", hops = 2
  ...
  Back to state 2.

If TLC does not flag this, the spec is wrong – the termination property is too weak or the ouroboros transitions are unreachable. The canary validates the validator.

The TLA+ model bounds hops at MaxHops. In production, the bound is imposed by the client. The core clients that matter for redirect validation:

The range is 10–50. Testing with curl (50 hops) exercises more of the chain than a browser (20 hops); Go at 10 is the most conservative.

Full empirical results across 13 clients (including Deno, Perl, Ruby, Crystal, Erlang, Elixir, Racket) with tangleable code blocks and server-side log verification: HTTP Redirect Limits: One Ouroboros, Six Languages.

For the wal.sh bot compliance spec (C6), redirect policy is deferred to v1.4.

Modeling web server configuration as a state machine is not standard practice. Most redirect debugging is done with curl -sIL and prayer. The closest related work:

• Lamport's framing of TLA+ as a tool for precise description: "the best way to describe things precisely is with simple mathematics" (lamport.azurewebsites.net/tla/tla.html). The .htaccess redirect system is simple enough to describe precisely and complex enough to compose badly – exactly the niche where specification pays off.
• Jackson's Alloy (Jackson 2012) models filesystem synchronization, access control, and protocol design – the same class of "small system, subtle composition" problem – but does not cover HTTP redirect chains.
• The Cloudflare/Rosette work presented at RacketCon 2025 uses formal verification for DNS configuration – the same class of problem (config-as- program, composition can diverge).
• The encode → transform URL migration on this site is a pragmatic case study: a phased redirect rollover with go/no-go gates, query-param preservation, and explicit rollback at every step. The RewriteRule it deploys is one of the transitions in this TLA+ model.

The novelty, such as it is, is applying model checking to the specific problem of Apache mod_rewrite rule interaction. The problem is both annoying (everyone who has debugged a redirect loop knows the pain) and well-suited to formal methods (finite state, deterministic transitions, clear safety property).