Tillandsias, explained simply

A tillandsia is an epiphyte, not a parasite: it rests on its tree and takes nothing from it.

What it is for, in one paragraph

The reason a grown-up wants one is narrower than "the cloud, but at home". Software you did not write — increasingly, AI assistants that write and run code for you — has to work somewhere. The choice is between your actual machine and a sealed room containing only the project folder you deliberately opened.¹ Tillandsias is that room, plus the plumbing to prepare it and start your tools.

Is my stuff private, and who could see it?

The people who make Tillandsias operate no servers your copy talks to: no account, no sign-up, no usage tracking, no crash reporting, no identifier attached to you or your machine.² Your logs stay on your own disk where you can read them, and leave only if you send them somewhere yourself. Any login you hand over goes into a secret store on your own machine — the project's own vault, whose key sits in your operating system's keychain, or on some hosts in a local file — never on anyone else's server.³¹⁶

Does it cost money? Does it need the internet?

It costs nothing: free software under a licence that lets anyone read, run, modify and pass it on.⁴ You have already paid for the only hardware involved.

The internet is needed only for ordinary, visible reasons: fetching the program, fetching updates, reaching a service you chose.¹⁷ Local work can continue without sending it to an AI provider: language models can run on your own machine.¹⁸ That does not make every action offline-ready. Fetching a missing tool or model needs a connection, and a push configured for GitHub fails when its upstream cannot be reached.³¹

What happens when I turn it off? Can it break my computer?

Turning it off is the expected motion, not an interruption. Anything you saved is a real file on your real disk, untouched by the rebuild. Even the internal secrets the pieces use to talk to each other are re-registered at every start, so yesterday's messy shutdown cannot jam today's start.⁵

Publishing your work has a rule that fits the same idea. Inside the sealed room you push to a mirror that lives on your own machine, not to the internet. The mirror passes the push onward and waits: it reports success only once the copy outside has durably accepted the same set of changes, so a success you can see is one that survives the room being thrown away.³² The mirror is also the only part that holds the credential for the outside service — it reads it when it pushes, and it never hands it to the room where your tools run.³³

As for damage: a misbehaving tool inside the sealed room sees only the folder you gave it.¹ Wiping the installation and rebuilding is documented and supported, not a last resort.⁶ The cost you do pay is ordinary and reversible — it is a real virtual machine, so it holds real memory while running and gives it back when it stops. The system image it downloaded stays cached on your disk so the next start is quick; uninstalling clears it, though on a Mac you have to ask for that explicitly.²⁰³⁰

Sharpening one thing you were told

You were told they check that nothing got worse. Precisely: the project's stated objective is that the measured gap between what it specifies and what it builds must not grow,⁷²¹ and its build gate refuses a change that points at a specification that does not exist, or that adds a new failing test — a machine's verdict, not a person's.²²²³

Two honest limits follow, in the project's own words. Passing tests are evidence, not proof — they show no contradiction was found, not that none exists.⁸ And "never worse" means settling toward some floor, not that the floor is zero; the stronger mathematical result that would guarantee zero is explicitly not claimed.⁹

Lots of small maps, one destination

An AI does not swallow a repository as one magic answer. It is given selected source, rules and a request; it suggests a small change; then people and tests decide whether to keep that change. Think of the selected material as a map, not as every file turned literally into a vector. The next job starts from the newly saved repository, so it can use what the earlier job learned.

Different jobs have different nearby destinations: a security repair, a clearer screen, or a working installer. They all share the larger destination of matching what the project promised. We can measure particular gaps and refuse a known regression,⁷²¹ but a row of successful changes is not proof that the whole journey reaches perfection.⁸⁹

Where it falls short today

Two install problems and one feature that once promised more than it delivered and has since been replaced. None touch the privacy story, and all three are here because the project's own checking found them.

Tillandsias, for a power user

Its roots only grip; the leaves do the drinking — a plant that runs rootless.

What you get the moment a forge opens

tillandsias --headless /path/to/project --claude starts a container with your project in it and an agent at the prompt. Nothing below is configured by you or by the agent: the context file the agent reads first lists the plumbing under the heading "all transparent — zero configuration needed".¹⁶ Every claim here is checked against the stable release, v56.9.12.2.

The forge container

A forge is a Fedora Minimal image in two layers: a heavy base carrying the toolchains — gcc, make, cmake, Rust with cargo and rust-analyzer, Go, Node, Java, Python, the debuggers — and a thin runtime layer with the entrypoints, cheatsheets and the agent's configuration.¹⁷¹⁸ The tag is a content hash of its sources, so an unchanged rebuild is a no-op.¹⁹ The coding agents are not baked in: every launch refreshes them into a per-project cache volume that outlives the container, rolling back to the last known-good version when upstream ships a broken one.²⁰²¹ Cheatsheets, /tmp and the runtime directory sit on RAM-backed tmpfs with hard caps.²² The default clone-only lane now puts the source tree on tmpfs too, sized from the mirror’s pack; the opt-in host-mounted checkout keeps its host mount.³⁰¹⁴⁹ Allowlisted commands — tmux and lazygit among them — are shims that install userspace Homebrew on first use.²³ On start the forge writes a context file into the checkout naming what is present, what is absent, and what needs no configuring.²⁴

The HTTPS proxy and its cache

Every container is born with its proxy variables set and the proxy's certificate composed into the system trust bundle before any network client starts; no per-client CA variable is set, and a regression test refuses a launcher that tries.^34353637 The allowlist of developer hosts — registries, GitHub, cloud SDKs, model providers — is generous enough that npm, cargo, pip and flutter work unconfigured.³⁸ It decrypts exactly one of them, GitHub's release-asset CDN, so a large asset is fetched once for the whole machine.³⁹⁴⁰ Everything else passes through encrypted, so the proxy never sees, and never caches, crates.io, npm, PyPI or api.github.com.⁴¹ What makes the second cargo build fast is not the proxy but a per-project cache volume for cargo, npm, pip and go that outlives the forge.⁴² A blocked host gets no 403: the connection is reset, and only the proxy log names the domain.⁴³

Local inference

The launcher prepares a shared model server at http://inference:11434, started on launch if it is not already running and shared across projects.^4546146 The first run pulls the engine and one small tool-capable chat model into a host directory that outlives the containers.⁴⁷⁴⁸⁹ Readiness is best-effort: a failed readiness wait warns and the forge launches anyway; errors while preparing the service can still fail launch.⁴⁶ The context file tells the agent, in a closed vocabulary, what the host's accelerators are and whether the endpoint is ready — ready means at least one model is cached, never "starting up".⁴⁹⁵⁰ Larger tiers are opt-in behind an environment variable; the CPU floor is unconditional by spec.⁵¹⁵²

The git mirror and push relay

For an agent, a refinement is a controlled data path: it receives selected source, rules, task context and tool results; it proposes a patch; local checks and review decide whether that patch becomes a commit. Git retains reachable commits, while the current tree is a snapshot that may replace or delete files. Calling the repository a "set of vectors" is therefore a useful description of the model's selected context, not Git's storage format and not a guarantee that every current file survives.⁶¹⁶²⁶⁶

Several tasks can run this loop at once. Each needs its own declared target and measurement; the shared repository is the coordination point, not evidence that their measurements are already comparable. The relay makes an accepted push atomic,⁶²⁶³ which preserves the record of what was accepted, not the truth of the patch.

Why this is built rather than borrowed. The mirror has to satisfy two requirements at the same time. The credential for the upstream must stay on the server side, so a workspace can publish its own work without ever holding a token that could publish anything else — the git service reads that token when it pushes and it never crosses into a workspace container.¹⁵² And the push must be synchronously durable: the hook relays the proposed ref transaction upstream before accepting it locally, so a client's success means the upstream has durably accepted the same atomic ref set.¹⁵³ The live relay performs that as a single atomic push.¹⁵⁴

Tools in general offer one of those or the other. A managed push mirror holds the credential for you and copies asynchronously, reporting success before the copy lands — which is precisely the false success that strands an agent's work. A caching or redirecting git proxy relays synchronously but forwards the client's credentials, which is the isolation being bought in the first place. Needing both at once is the unusual requirement, and it is what the pre-receive relay exists to provide.

Rolling the decision back is deliberately cheap: the relay is a bare repository plus a pre-receive hook, so undoing it means pointing the daemon back at the bare repository.

Git needs nothing from you inside a forge. A read-only global gitconfig redirects the project's GitHub URL to a bare mirror in its own named volume, so git remote -v still says github.com while clone, fetch and push hit the enclave.⁶¹⁶ A push is not acknowledged until the mirror's hook has relayed exactly those refs upstream with one atomic push.⁶²⁶³ The token authorising that relay is read from the vault inside the git service at push time and never enters the forge.⁶⁴⁶⁵ Deletions and branch rewinds land nowhere;⁶⁶ a project with no upstream keeps its pushes in the mirror.⁶⁷

The vault

Secrets live in a Vault container at vault:8200, reached over TLS with the enclave certificate already trusted.⁷⁴⁷⁵ A lane with a credentialed provider is handed a single-purpose token on tmpfs at /run/secrets/vault-token whose policy reaches only that provider's paths; the generic forge policy cannot read the GitHub token, which the git mirror, the tray and the login flow can.^76777879 Across a stop, Vault unseals itself from one Shamir share held in your host keychain, with no passphrase prompt.⁸

The experts and the project index

The agent finds four tool servers already registered, for Claude Code and OpenCode alike: git tools, a project index, the host-browser bridge, and a plan expert.⁸³⁸⁴ The index answers project type, status, commands and layout for any checkout, citing what it indexed; the plan expert returns cited answers or a typed refusal, never a guess, and answers only on a checkout carrying Tillandsias' own plan crate — elsewhere it reports itself degraded, by design.⁸⁵⁸⁶⁸⁷ Both start in the background after the clone and never gate the session.⁸⁸ The status now distinguishes the running expert’s capabilities from what a relaunch would build: waiting for a build, needing a relaunch, and losing capabilities on relaunch have different machine-readable verdicts.¹⁵⁰ A ready index is separate from a usable answer engine. Deterministic project questions can work without local inference; synthesis still returns a typed refusal when the synthesis capability is absent, even if inference itself is ready.¹⁵¹ The "on-demand" spec describes tray-side spawning and health checks that do not exist; the harness launches each server itself.⁸⁹

Sibling web containers

Ask the agent to publish the project and it does not start a server in the forge. It asks the host, over a socket that exists only for that lane, to launch a sibling: a busybox httpd with the project mounted read-only, joined to the enclave network and given a router route.^93949596 The URL comes back as http://www.<project>.localhost:<port>, fetchable from the forge through the proxy.⁹⁶⁹⁷ The project is attributed from the socket the request arrived on, never from the request.⁹⁵

Chromium

Two browser images are built at initialisation: a minimal headless core, and a framework layer on top of it with GUI Chromium, Node and Playwright.^101105106 The runtime launches the framework image as a read-only, capability-dropped, incognito app window — but only for the OpenCode-web and observatory modes, and only on a machine with a display.¹⁰⁷¹⁰⁸ The browser tool the agent sees — open, screenshot, click, type, close; eval switched off — is a different thing: it drives a host Chrome from the user's cache directory that nothing shipped installs, so a fresh host answers "browser unavailable".^109110111112

The anatomy

The region is one Fedora guest — a VM, or a WSL2 distro on Windows — running a rootless Podman stack. Among the members:

• a forge, the container your coding agent runs in, one per project;
• a git mirror, a bare repo on the internal network;
• a vault holding your tokens;
• a forward proxy, the single outbound door;
• a router, a Caddy reverse proxy giving web services stable names;
• an inference container, the shared model server.

The roster is longer — a Nix cache, a catalog service, the observatory's web container, an SSH-lane sidecar — and most of those do not run in an ordinary session.¹ Membership is not a hand-kept list: the spec names the attach sites by function symbol, and a guard compares the attach sites it finds in the source with that list, refusing the build if either side drifts. It reads code, not a live network.¹³²

One rule carries the isolation: the containers share a Podman network created with --internal — no gateway, no route out.¹ Only the proxy is dual-homed onto an egress network, and the launcher creates both networks on the first launch and reuses them after.¹³¹

The router publishes to one loopback address — port 80 by default, with fallbacks, or the port you pass with --port — and maps <service>.<project>.localhost onto internal ports. Nothing binds 0.0.0.0.²¹¹⁶

Starting one is a curl on Linux, an installer script on macOS, a tray executable on Windows. Then tillandsias --headless /path/to/project --claude.

What the walls are made of

Agent tooling exists only inside the forge image, never on your host $PATH; a missing image makes the launcher refuse rather than fall back to a host binary.⁴¹²² Mounts are enumerated — your project, a read-only CA certificate, the tmpfs roots, a per-launch temp dir, the persistent tool-cache volumes and a Tillandsias-written read-only gitconfig — so $HOME, ~/.config and your keychain are simply not addressable from inside, and a regression test asserts no user home is ever mounted.⁵

The forge does not touch your working tree by default: it clones fresh from the enclave mirror, and pushes travel back through the mirror on their way upstream.¹²³¹²⁴ An opt-in escape hatch bind-mounts your real checkout read-write and prints a reduced-isolation warning.¹²⁵ Hence the blunt operating rule: a finding you did not push is a finding you destroyed.⁷

What survives, exactly

Idempotence is what makes destroy-and-recreate a repair procedure rather than a loss. Every layer comes up clean from scratch, so the boundary worth memorising is not "will it break" but "what is on which side of the wipe":

• Survives a stop: the bare mirror in its per-project volume, with everything you pushed to it.⁶
• Survives a stop: vault data, auto-unsealed from a single Shamir share held in your host keychain, with no passphrase prompt. The spec requires the share to reach the vault only through a tmpfs-mounted secret;⁸ the shipped guest also keeps a fallback copy of the share on its own disk when no keyring is reachable, and inside a VM guest that file is written on every initialisation.¹²⁶¹²⁷
• Survives even podman system reset, on Linux: the model cache, because it is a host bind mount and not a named volume. The spec spells that distinction out, having once cost someone a wrong answer.⁹
• Does not survive --reset-guest: it wipes the vault and every enclave container, volume, secret and network, then re-initialises, keeping the model cache. Push first.^10128129

Driving it, and where the gate sits

The verification the earlier levels described is, operationally, a local gate: specs declare intent, litmus tests turn each requirement into an executable signal, traces prove the signal ran, and the gate refuses a push that breaks the chain. Two things follow that change how you work.

First, read a green gate with care. Eleven litmus files sit on disk and have never been executed by any suite — grandfathered onto a shrink-only list so that switching the gate on did not flip them all red at once.¹⁴ The list may shrink; nothing may join it.

Second, the gate on your machine is the only gate there is.

Tillandsias, for an IT / security reader

Silvery leaf scales open to take water in, then trap air to keep it: every exchange across one surface.

Where the boundary actually is

The anatomy does not answer the security question: when an agent does something you did not intend, how far does it get?

First, a correction. The region was described as one Fedora guest — a VM, or WSL2 on Windows. True on two platforms, false on the third: Linux provisions no VM, and the orchestrator drives rootless containers directly on your host.¹ The promise is that this costs nothing but Podman; the price is that the enclave is a hypervisor boundary on macOS and Windows and a namespace boundary on Linux — where an escape lands as your own uid, with your $HOME.²

Inside, every launch is meant to carry four flags — userns mapped to your uid, all capabilities dropped, no-new-privileges, and label-disable, which is to say SELinux labelling off on every container — audited by a policy module that rejects privileged mode, a non-identity userns, or a blanket capability add.⁴⁹⁸ Why this envelope: keep-id makes an escape land as you rather than root, and a checker that never runs Podman is one small place to ask whether a launch still carries it. The compromise is the fourth flag, bought so bind mounts work on an SELinux-enforcing host.⁹²⁹⁴ Read the envelope as defaults on a struct, not an invariant — and not quite every container: the vault adds one capability back, omits --rm, and never passes the checker at all.⁵³

The litmus now derives its launch flags from the product's declared envelope.⁵⁸ Its repaired user-namespace probe checks ownership of a host-owned mounted file, because inspecting the namespace label or comparing the process uid alone could give a misleading answer.¹⁰⁰ That is evidence about the declared envelope and Podman on the tested host, not proof that every production launch uses it.

Egress: intercepted versus passed through

The intended egress boundary is network placement plus proxy environment variables. The proxy configuration supplies hostname rules; it does not establish that the host or container networking stack uses no packet filters. An agent can unset HTTP_PROXY; what stops it is that the namespace has nowhere to send the packet. Then the question everyone asks on hearing "trusted CA in the container":

The cost of that restraint: with one host decrypted the proxy does no payload inspection — hostnames, not content — and its default-deny allowlist admits anyone-can-publish namespaces, so an allowlist hit is no evidence of a benign destination.³³⁰ What it buys is a denial that looks like a network fault: a refused runtime request gets a TCP reset, not a page to negotiate with — the config's behaviour; the spec still promises a 403.³⁷³⁸

Secrets, and the channel that guards them

The GitHub token never enters the agent container: the mirror holds short-lived role credentials, relays pushes on the agent's behalf, and passes the credential on stdin rather than argv, closing a process-listing leak. One clause on the relay: it wires the GitHub helper for any HTTPS origin and the helper answers unconditionally,⁴⁸⁴⁹ so the origin decides where the token goes.

Why the relay is bespoke, in security terms. The design needs the upstream credential to stay server-side and the push to be synchronously durable, and those two requirements pull against the available tools. A managed push mirror holds the credential and copies asynchronously, so it reports success before the copy lands; a caching or redirecting git proxy relays synchronously but forwards the client's credentials, dissolving the separation this section is about. The hook takes the third option: it relays the proposed ref transaction upstream before accepting it locally, so a client's success means the upstream durably accepted the same atomic ref set.¹⁰⁷

That is a security property and not only a convenience. A false success is indistinguishable, to the agent that received it, from work that is safely published — so an asynchronous mirror would put unpublished work behind a green light, on exactly the disposable machine the design expects to be thrown away.

The host↔guest control channel now uses a Noise handshake by default. Its key is derived through HKDF from the guest binary's SHA-256, separated by build version, wire version and hop.¹⁵¹⁰³ This binds compatibility to known release material; it is not remote attestation that the peer runs unmodified code.

A release exposed a second boundary: the tray and guest are different executables, so hashing each process's own binary produced different keys even at the same version. The host now derives its key from the guest digest embedded at build time, while the guest hashes itself.¹⁰³¹⁰⁴ The Windows caller refuses a missing embedded digest and includes tests for matching and mismatched guest digests.¹⁰⁵¹⁰⁶ A one-process round-trip test could never have detected the original two-binary mismatch; that limitation is now recorded beside the implementation.¹⁰⁴

Supply chain and provenance

Where ephemerality stops being a control

Ephemerality resets compute, not identity. Of what survives teardown, the security-relevant item is the Vault unseal share, which lives in the host OS keychain — outside every boundary the enclave draws.²² The reason is fair — no passphrase prompt, never wipe a vault the host can still open — but destroying the region does not destroy the ability to open what it held.

Blast radius, autonomy, auditability

An agent's reach: its forge, every mirror on the enclave network, any allowlisted hostname with nothing inspecting the payload. Not your keychain, $HOME, or real checkout — unless you took the host-mount escape hatch.

The audit trail is committed and unusually candid. It is also agent-self-reported and unsigned, with no commit signing evidenced: a tree once passed green while red, and the repo calls its own fix unforgeable by accident, not by intent.⁹⁹ With nothing in this repo evidencing server-side validation of a push, the record's provenance rests on the honesty of the process that wrote it.

What the assurance claim actually is

The convergence argument you already have is not a security argument, and the project does not offer it as one. What carries the weight is a pair of invariants — verification claims must be falsifiable, and evidence is not proof²⁵ — plus the methodology's refusal to read its completion score as a probability.²⁶ So: a passing suite is a bounded signal over the defects someone thought to write a litmus test for, and, as the hardening case shows, only over those whose tests distinguish the relevant failure from success. Finite litmus coverage is not proof of absence of defects; the repo says so before you do.

Security is one local target among several. An agent may add a check, a boundary or an audit record to the shared repository, but that does not make the next change independent, nor does it turn a passing security test into a statement about every other target. The useful engineering loop is narrower: make the claimed boundary explicit, try to break it, retain the evidence and record the counterexample when it fails.²⁵²⁶

Level 5 — For the MathWiz / Hacker

A monocot bromeliad flowers once and dies, leaving offsets behind — the pup is never the parent.

The lower levels gave you the object and its defects. What is left is the only part that can be attacked with a pencil: the formal content, stated as claims with hypotheses, sorted into (a) standard theorems being invoked, (b) what the repository actually asserts, (c) what follows, and (d) what does not. The security findings of level 4 are not repeated; they enter here only where a mathematical hypothesis depends on them.

The short verdict: the theory is small, finite, and unusually candid about the theorems it declines to claim. Its model now has generative property tests and stable requirement identifiers. Connecting those checks to live validation and justifying dependent iteration remain separate obligations.

The lattice, and the one step worth checking

An obligation is a named, auditable requirement, invariant, litmus signal, trace signal, provenance binding, or environment assumption carrying a stable identifier¹. Its state ranges over a finite chain, seven long²:

Fix the convention, since authors differ: the height of a finite poset is the maximum number of strict order steps in a chain — so a chain of \(n\) elements has height \(n-1\), and the one-element poset has height \(0\).

Proposition 1. \(S_{\text{proj}}\) is a finite complete lattice of height \(6|\mathrm{Obl}|\). Each \(\mathcal{O}_i\) is a finite chain, hence a complete lattice; a finite product of complete lattices is complete with \(\vee,\wedge\) computed componentwise; a chain of seven elements has height six and heights add over products³. Nothing here is in dispute — it is the least interesting true thing in the file, and the repository correctly declines to inflate it: "this proves monotonicity of the model, not truth of the modeled requirement or adequacy of the chosen obligation set"⁴.

Two hypotheses do quiet work. The order is componentwise after aligning stable IDs and tombstones¹, so a renamed coordinate yields a different lattice, not a lower point in the same one; and \(|\mathrm{Obl}|\) must be finite and known, which is what makes the height bound a bound rather than an ordinal.

The fixed point, in full

Let \(\mathrm{refine}: S \to S\) be validation followed by semantic distillation at a fixed bar \(B\). The repository's stated claim is idempotence⁵:

Theorem 2 (Knaster–Tarski). A monotone map on a complete lattice has a complete lattice of fixed points, in particular a least one⁶. Applied here it gives existence, non-constructively, and says nothing about how to reach it.

Theorem 3 (finite monotone inflationary iteration). If \(f: L \to L\) is monotone and inflationary (\(x \le f(x)\)) on a finite lattice of height \(h\), then for every \(x\) the chain \(x \le f(x) \le f^2(x) \le \cdots\) stabilises after at most \(h\) strict increases, and its limit is the least fixed point \(\ge x\). The bound is immediate: each strict step rises at least one level in a poset of height \(h\). Leastness is a two-line argument worth doing, because it is the step people skip: if \(y = f(y)\) and \(y \ge x\), then monotonicity gives \(f^n(x) \le f^n(y) = y\) for every \(n\), so the limit is \(\le y\).

Note where Kleene's theorem proper — least fixed point as \(\bigsqcup_n f^n(\bot)\) for a Scott-continuous \(f\) on a CPO⁷ — would otherwise be invoked outside its hypotheses. Continuity is not assumed, it is free: in a finite poset every directed subset is finite and contains its own supremum, so every monotone map is Scott-continuous. That is the first place a referee probes, and it survives.

So "done" is a computable predicate — \(x\) is closed iff \(\mathrm{refine}(x) = x\) — and governance supplies the hypothesis that makes it non-vacuous: the bar \(B_v\) is fixed within a release, rising only by explicit operator decision, with the automation forbidden from self-escalating it⁸. A continuously rising bar makes \(\mathrm{refine}\) a moving operator and destroys stabilisation; discrete, externally gated raises preserve it. That is the standing hypothesis of Theorem 3, not decoration.

And now the gap. Theorem 3 needs monotone and inflationary; the repository asserts idempotent. These are the three axioms of a closure operator, and the repository states one of them. Idempotence does not imply monotonicity: a map that sends \(a \mapsto \top\), \(b \mapsto b\) with \(a < b\) is idempotent and not monotone. Nor does it imply inflationarity. The validation program that would discharge the missing two is written down — enumerate the allowed transitions and property-test that each is order-preserving for every affected obligation⁹ — which is the right shape of obligation. That program now has executable tests over a committed rule set; it does not establish the same properties for every live validator⁴¹.

The moving target, and what would force the floor to zero

Write \(T_v\) for the specifications at version \(v\), \(I_v\) for the implementation, \(d_v = d(I_v, T_v) \ge 0\). Because the specifications evolve, \(T\) moves and no final target exists¹¹. The mechanically checkable release rule is non-increase.

Proposition 4 (monotone convergence). A non-increasing real sequence bounded below converges to its infimum¹². Here:

That is the whole result, and it is correct.

What does not follow is \(d_* = 0\), and the repository says so in those words¹¹. The exact extra hypothesis is a uniform progress premise, in either of two forms:

Either excludes positive residual fixed points and forces \(d_* = 0\) — the additive form in finitely many steps, the multiplicative one geometrically. The repository's phrase — "a validated progress premise that excludes positive residual fixed points"¹¹ — is precisely this, asserted as a requirement on a future claim rather than as a fact.

The Banach alternative, itemised. A contraction claim¹³ would owe a complete metric space \((X,d)\), an operator \(F: X \to X\), and a constant \(0 \le c < 1\) with

Missing: (i) a metric, (ii) completeness, (iii) any bound on \(c\). The repository lists all three¹⁴. The binding one is (i), and it is worse than "unproven". \(d\) as used is not a function on \(X \times X\) at all — it is only ever evaluated at the single pair \((I_v, T_v)\), giving a sequence of numbers indexed by release, not a binary function on a set. Ask which axiom fails and the honest answers are:

The first two are undefined rather than false, because \(d(x,y)\) for two arbitrary project states is never given a value; identity of indiscernibles fails outright, since two materially different implementations can close the same obligation set and score residual zero. Absent (i), items (ii) and (iii) are not merely unproven — they are not well-posed. Until a metric exists, "monotonic convergence" means ordered non-regression plus finite residual descent, which is what the file claims and no more¹⁴.

Be careful about the scope of that verdict, because it is easy to overstate and I will not. Everything above concerns the \(d\) the repository actually documents. It is not an argument that no suitable metric exists on project states, and nothing here forecloses one: a genuine metric — with a completion, and a contraction constant — may well be constructible, and if it were, the Banach route would reopen exactly as written. The claim is the narrow one. The contraction argument cannot be discharged by the object currently on offer, and the work of building a better one is open rather than blocked.

There is a further boundary. Under a fixed denominator, a non-increasing integer residual is eventually constant; strict progress while positive would force zero. Changing the obligation scope breaks that comparison. A ratio alone cannot repair it: adding easy obligations can improve the percentage without closing an old gap.

A repository refinement is a model, not a theorem

Here is the engineering picture in a form precise enough to attack. Let \(R_k\) be the repository state visible to a task, \(p_k\) its prompt and \(C_k\) the selected context built from source, rules, retrieved material and task state. A model proposes a delta \(Delta_k\); review and validators decide whether to commit it:

"Vectors" is a useful picture of the representations the model constructs from \(C_k\); it is not Git's data model. A commit can retain reachable history while its new tree replaces or deletes files. Nor is an accepted patch automatically an improvement. The acceptance step is where tests, review and evidence enter; the finite obligation model says exactly what those validators can record, and no more.¹⁴⁰

For a workstream \(i\) with a fixed specification \(T_i\), write \(d_i(R_k,T_i)\) for its declared, measured residual. Accessibility and language, marketing, dashboards and customer support may each have their own \(d_i\). A shared residual is meaningful only after the obligation identities, weights and scope have been aligned; tombstoning already marks the shipped scorer's comparison as broken.⁴⁴⁴⁵ Thus the diagram's local traces are engineering telemetry, not samples from a common distribution.

The tempting probabilistic upgrade is to treat \(Delta_k\) as one random refinement with a finite-step skew, then invoke a weak or strong law over many refinements. That argument needs a stochastic model of the quality functional, a target mean and conditions on the joint process. Large context windows, high-dimensional embeddings and a fresh prompt do not supply independence. The next input contains \(R_{k+1}\), which was made using the previous output; this is feedback, not a negligible detail. The possible formal routes are the ones below: establish a dependence structure that supports an ergodic or martingale theorem, or leave the claim empirical.¹⁶¹⁸¹⁹

Iteration: the law of large numbers at full strength

The methodology now withdraws its strong-law citation for dependent iterations¹⁶. The mathematics below explains why that correction matters. Set it up properly. Let \((X_k)_{k\ge1}\) be random elements on a probability space, \(X_k\) the value of a real quality functional on iteration \(k\), with \(\mathbb{E}|X_k| < \infty\) and \(\mathbb{E}[X_k] = \mu + b_k\), where \(b_k\) is the per-iteration skew. Write \(\bar{X}_N = N^{-1}\sum_{k \le N} X_k\) and \(\bar b = \lim_N N^{-1}\sum_{k\le N} b_k\) when that limit exists.

Theorem 5 (Kolmogorov's SLLN). Under independence, identical distribution, and integrability¹⁷:

The iterations here are not identically distributed, so a candidate generalisation is Kolmogorov's variance criterion, which drops identical distribution and keeps independence¹⁸:

Same family as the three-series theorem; independence and the summable-variance condition are the whole price of admission.

Weak versus strong is convergence in probability versus almost-sure convergence; almost-sure convergence implies convergence in probability, but the converse need not hold. Under the criterion above and existence of the mean-bias limit, bounded bias bounds the limiting error. Bounded bias alone does not imply convergence, and unbounded skew does not by itself prove divergence. The methodology retains small, fast iterations as engineering guidance while withdrawing the almost-sure claim¹⁶.

The objection the methodology now acknowledges is the load-bearing one. Every form of Theorem 5 quoted above requires independence. Iterations of an agent that reads its own prior output are not independent: \(X_{k+1}\) is a measurable function of \(X_k\) and the accumulated context. The architecture makes the dependence explicit and deliberate — retrieval is a cache of converged knowledge, updated on commits, with commits acting as a Lamport clock ordering the corpus against the code¹⁹. That is a feedback loop by construction, and it invalidates every independence hypothesis in the section above.

Two possible substitutes remain unestablished. Either the sequence is stationary and ergodic and one invokes Birkhoff's pointwise ergodic theorem²⁰ — but stationarity is implausible for a process whose corpus grows monotonically, and ergodicity is exactly what fails if the chain can be absorbed. Or the increments form a martingale difference sequence with respect to the natural filtration \(\mathcal{F}_k = \sigma(X_1,\dots,X_k)\), giving an \(L^2\) or Azuma-type law — but that requires

which is precisely the assertion that yesterday's output does not bias today's, and the cache design says it does. Under positive feedback an absorbing state is available: the stream converges almost surely to whatever the loop locked onto, and \(\bar X_N\) converges beautifully to a number with no relation to \(\mu\). Bounding per-prompt skew does not repair this; it is a hypothesis about marginals, and the failure is in the joint.

Be precise about what this objection kills. It does not show the iteration scheme is wrong, and it does not show the stream fails to converge — small fast iterations may well be the right engineering, and dependent sequences converge under plenty of other hypotheses. What it kills is the invocation of the strong law as stated: the theorem named is being applied to a sequence that does not satisfy its independence hypothesis, so the almost-sure conclusion is unearned rather than false. The repair is cheap in words and real in work — name the dependence structure, then cite the theorem that covers it.

What the repository renounces, and what that costs

No Galois connection. Specs and scores are described as abstractions that deliberately forget detail — the Cousot framing²¹ — and the file concedes that no adjunction is defined between program semantics and spec obligations²². State the missing object precisely. With \(C\) the lattice of sets of concrete executions and \(A\) the obligation lattice, a Galois connection \(\alpha \dashv \gamma\) requires monotone \(\alpha: C \to A\), \(\gamma: A \to C\) with

What is forfeited is the transport theorem, and only that — but that is everything. Given the adjunction and a sound abstract operator (\(\alpha \circ F \sqsubseteq F^\# \circ \alpha\)), one gets \(\alpha(\mathrm{lfp}\,F) \sqsubseteq \mathrm{lfp}\,F^\#\): a fixed point computed in the abstract over-approximates the concrete, so a property proved upstairs holds of every concrete execution downstairs. Without it, closure in the obligation lattice implies precisely nothing about the program. It is bookkeeping over evidence, and is labelled as such.

A ranking function, not a measure. The CentiColon map \(c: S_{\text{spec}} \to \mathbb{N}\) is bounded, with separately reported denominator and residual, and monotone only for transitions preserving obligation IDs and introducing no penalties, ambiguity, or denominator scope change¹. That is a Floyd-style ranking function²³: a well-founded descent witness into a finite ordinal, of the kind that proves termination.

It is not a measure. There is no \(\sigma\)-algebra on \(S_{\text{spec}}\); \(c\) is not additive, because obligations overlap and sixteen penalties plus six cap rules make the rollup non-linear in its parts¹⁵; and the normaliser is policy rather than a fixed total mass. A bounded ranking function into a finite ordinal therefore induces no probability, and the repository says so outright²⁴. What that forecloses is concrete: two scores may not be combined by Bayes; there is no complement rule, so 89% closed is not an 11% chance of a defect; and no calibration statement is available, because there is no event space on which to calibrate. Shafer²⁵ and Walley²⁶ are cited as the layer a confidence model would have to occupy separately — correctly, since a belief function would at least supply the monotone-capacity structure that \(c\) lacks.

That is a statement about \(c\) as defined, and about nothing more. It does not show that no transformation, extension or added structure could turn part of this model into a measure or another probabilistic object — the citation of belief functions is precisely an admission that such a layer is available to be built. What is claimed is that \(c\) does not already carry that structure, so probabilistic language applied to today's scores is unlicensed. Building the layer that would license it is open work, and the repository files it as such.

CRDTs as algebra

The plan ledger is a genuine convergent replicated data type. State is \(\text{base} \oplus \mathrm{fold}(\text{fragments})\); the carriers are two join-semilattices³¹: grow-only sets of packets and of events keyed by \((\text{packet id}, \text{event identity})\), with \(x \sqcup y = x \cup y\); and last-writer-wins registers per \((\text{packet id}, \text{field})\), the winner chosen by the total order \((\text{timestamp}, \text{host})\).

The algebra: a commutative, associative, idempotent \(\sqcup\) induces a partial order \(x \le y \iff x \sqcup y = y\) under which \(x \sqcup y = \sup\{x,y\}\) — the join is the least upper bound, which is why the three properties are a definition rather than a checklist. Convergence follows because the fold is then a function of the set of delivered updates, not their sequence: idempotence kills duplicates, commutativity and associativity kill order.

State exactly what that buys, because it is strictly less than the folklore suggests³². It gives: replicas having delivered the same update set hold equal state. It does not give delivery — liveness is someone else's problem; it does not give correctness of the converged value; and it does not preserve concurrent intent, which is where LWW does its damage. Applying LWW to a list silently discards the loser's entries, which is why events are a set and not a register — a distinction the file calls the whole correctness argument³¹. Determinism is pinned by folding in \((\text{timestamp}, \text{filename})\) order rather than directory order³³, and two of the three properties — commutativity and idempotence — are tested by name³⁴.

The status field is not a plain register: it composes a monotone join over a closure rank with LWW as tiebreak at equal rank, treats terminal-but-lateral values as non-ladder moves, and permits descent only under an explicit falsification flag³⁵ — a lexicographic join with a deliberate non-monotone escape hatch, so that monotonicity cannot force retention of a certainty later shown false.

Verdict

The formal core is a finite product lattice, a finite monotone-inflationary stabilisation under declared validators at an operator-gated bar, a Floyd-style ranking function, and a correctly stated moving-target result whose zero-floor corollary is declined for want of a metric. Contraction, Galois connections and probabilistic readings are named absent rather than assumed⁴⁰. As a thesis position that is defensible, and I did not expect to write that sentence.

Two boundaries remain. Generative tests cover the committed refinement model, not the semantic correctness of all live validators. And dependent iteration still lacks a convergence theorem, although the methodology now retracts the unsupported strong-law claim. Stable identifiers and centralised score arithmetic make the bookkeeping more concrete; they do not turn closure into probability or a dashboard snapshot into release evidence.