5.3 The Built System

This chapter illustrates

✓ The Modeling Thesis · ✓ The Alignment Thesis

The timeline told what happened. This chapter tells what got built, because none of the governance in the rest of the book makes sense until you can see the shape of the thing it governs. DocAble is a real system, live in beta: hand it a document a university actually distributes and it hands back a version a screen reader can read. Frontier models do the parts that require understanding a slide; ordinary deterministic code does everything else. The interesting engineering lives in how those two halves are joined.

5.3.1 What the system does, end to end

A user uploads a file. The system figures out what kind of document it is, breaks it into work, remediates each piece, checks the result against a real accessibility standard, stamps what it changed, and returns the corrected file with evidence that the job was done. Six moving parts carry that load.

• A front door. A website and an API take the upload, authenticate the user, meter the usage against a quota, and put the job on a queue. A professor drops in a slide deck; the system takes it from there.
• A dispatcher. The document is split into chunks — slides, pages, sheets — and each chunk becomes a unit of work handed to a worker. Splitting is what lets a hundred-slide deck finish in about a minute instead of an hour.
• A remediation core. A command-line engine, written in a typed language, does the actual repair. It walks the document through a structured model of its format, and for each thing that needs fixing it either applies a deterministic rule or asks a model. This is where alt text gets written, reading order gets set, titles get added, contrast gets fixed.
• A check engine. After every pass, a standards-grounded checker maps each remaining finding to a specific clause of the accessibility standard, so the system owns the definition of done rather than trusting an outside tool.

Learn more about this governance mechanism: standards-grounded check engine.

• A fidelity validator. The fidelity validator introduced earlier sits here, catching the file that came out more accessible and less true.

Learn more about this governance mechanism: fidelity validator.

• A provenance layer. The provenance layer from the pipeline stamps every insertion, giving a document the auditable trust a university requires.

Learn more about this governance mechanism: per-mutator provenance stamps.

Those six parts are the product. What surrounds them is larger. In the talk this book grew from, I put the code-to-test ratio provocatively: the industry is happy with one line of tests per line of code, and I had one-to-four. The real recorded figure across the whole tree is close to that in spirit — the support apparatus, tests and lints and models and load-bearing documentation together, runs about 3.0 times the size of the production code. Call that inversion gold-plating if you like — but the more code the fleet produces, the smaller the fraction of it any human reads, and at this volume no one reads the diffs at all. The apparatus is the review.

Two design commitments run underneath all six. Every format is touched through one structured model, never the raw library, so a fix applied once holds everywhere. And the system fails loud: when the model is unreachable, the pipeline stops rather than quietly shipping a degraded file.

Learn more about this governance mechanism: one structured model per format.

5.3.2 The document is the hard part

None of this would be worth building if a document were merely text in a box, and of course it is not. A slide is a visual and semantic artifact — figures, tables, equations, an order the eye follows, emphasis carried by layout and color. To make it accessible, the system must recover enough of that meaning to present it through another channel. For years that was out of reach. The turn came with vision-language models that can look at a rendered slide and say what it means: read the equation, describe the figure, name what the slide is trying to teach.

That capability is real, and it is not a system. You can paste a small deck into a chat model and get useful output. You cannot get a corrected file back, a guarantee it satisfies the standard, or any evidence the meaning survived the trip. The model understands the slide and understands nothing about the file format, the standard, the university, or the cost of being wrong. Turning that flash of capability into something a university can trust is the engineering. The next section gives the pattern that does the turning.

5.3.3 Designing with a probabilistic component: the LLM as a function call

A model is a probabilistic component. Ask it the same question twice and you may get two answers. Ask it a question slightly outside what it saw in training and it will answer anyway, confidently, wrong. A deterministic function you can reason about; a probabilistic one you cannot. And yet the model is the only thing that can look at a figure and describe it. You have to build a reliable system out of an unreliable part.

The pattern that makes this work is to treat the model as a typed function call. Deterministic algorithms control the workflow and define the objective of each step. When a step needs semantic understanding, the system delegates a bounded task to a tool-equipped model — then a deterministic module validates the returned artifact before it is allowed in. The workflow is deterministic. The model is a subroutine inside it. The subroutine is never trusted on its word.

The same pattern, in another domain — and its lineage. The shape is old and rigorous. Proof engineering separates the untrusted work of writing a proof from the trusted kernel that checks it: the kernel, not the author's confidence, decides what is admitted. Ringer and colleagues survey what it takes to make formally verified software scale: proof organization, automation, and maintenance ¹1. Talia Ringer et al., “QED at Large: A Survey of Engineering of Formally Verified Software,” Foundations and Trends in Programming Languages 5, nos. 2–3 (2019): 102–281, https://arxiv.org/abs/2003.06458.. Recent systems put a language model inside that loop, letting it search for proof structure while a prover returns counterexamples and admits only a closed proof ²2. Haoxin Tu et al., “Agentic Verification of Software Systems,” 2025, https://arxiv.org/abs/2511.17330.. Our own AutoSOUP is one: it verifies component-level memory safety by representing scope, loop bounds, and environment assumptions as explicit unit-proof artifacts, delegating bounded inference through an LLM-as-function-call architecture, and validating each choice against the verification objective ³3. DocAble Research Group, “Deterministic Workflows with Bounded Model Delegation for Software Verification,” 2026, https://arxiv.org/abs/2605.10712..

MAGE carries the same trust boundary out of the proof assistant and into ordinary production. The external authority need not be a theorem prover. It can be a type system, a semantic lint, a preservation check, an architecture gate, a conformance engine, or a deploy rule. What must not blur is the guarantee each one carries: a lint proves less than a verifier, a preservation check proves only the property it encodes, and no green local check certifies the whole system. The untrusted generator paired with a trusted checker is not MAGE's invention; MAGE's move is to compose that one shape across the whole line.

Read the pattern in three moves, drawn in Figure 5.3-1.

• The caller is deterministic, and it owns the workflow. Ordinary code decides what happens and in what order. It decides when a step needs the model at all — most steps do not. When a step is a matter of judgment rather than a matter of rule, and only then, the caller reaches for the model.
• The call has a typed contract on both sides. The task handed to the model is packed into a typed input — this figure, this context, this question — and the answer must come back in a typed output shape the caller can act on. The return value is a structured, checkable artifact, never a free-form paragraph.
• A deterministic validator sits at the trust boundary. The model's answer is a candidate, not a result. Before it is incorporated, deterministic code checks it: does it satisfy the standard, does it preserve the input's meaning, does it fit the contract. On a pass, the caller incorporates the candidate and moves on; on a fail, it retries or falls back.

This is why DocAble can make a defensible claim on top of an infinite midwit. The model supplies the one thing deterministic code cannot: it looks at the figure and understands something. Everything around that understanding — when to ask, what to ask, whether to believe the answer — stays in code you can reason about and test. The probabilistic part is sealed inside a bounded call with a check on the way out.

This discipline was earned the hard way. Skip the wrapper and the model will find the exception you did not guard — I assure you. Agents are the fastest road to a working demo and the fastest road to a subtle, confident, wrong result. The function-call shape keeps the first from becoming the second.

5.3.4 Three views of the same system

A model shows a view. The sections below draw three architectural views of DocAble from its real system models. Each answers a different question. The first asks how the services are shaped, and why that shape let the whole system change its deployment target without a rewrite. The second asks how the front end is decomposed, and how the editor changes a document through a small edit language. The third connects that edit language to the automated pipeline, and shows the join as a concrete instance of the function-call pattern above. Read together, they are the standing structure the rest of the book governs.

5.3.5 View 1 — a reactive service seam, and how it made serverless natural

The back end is a set of small services wired to react to events. A user's upload lands at a web front door, which splits the document into chunks and enqueues each chunk as a unit of work. A queue hands each chunk to a stateless worker. The worker remediates its chunk and publishes a completion. A fan-in step collects the completions and assembles the finished file. Every hop is an event handed forward, not a component polling for work. Two commitments hold the seam together: services stay reactive and stateless, and the split of duties is declared — Redis carries communication, the database carries truth. Figure 5.3-2 draws the seam and the two ways it deploys.

Learn more about this governance mechanism: service-flow model.

That shape is what made a hard migration easy. For most of the system's life the workers ran on a Kubernetes cluster, and the dispatch worked by poll: workers reached into size-stratified Redis queues and claimed the next chunk, while a custom autoscaler watched queue depth and added or removed worker pods. The cluster billed around the clock, which for a bursty, low-traffic product was the wrong cost shape. The fix was to move to a serverless push plane: a managed task queue hands each chunk to a worker that scales from zero, a managed topic fans in the completions, and the platform's native autoscaler replaces the custom one.

In the industry a re-platforming like that is a quarters-long migration with a rewritten coordinator and a nervous cutover. Here it was close to a change of deployment target. The reason is the seam. A reactive, input-triggered handler is the serverless execution model (an event in, work out), so the workers did not need new logic to be pushed to instead of polling. A stateless worker can be spun up on demand and thrown away, because it carries nothing between invocations. And the split that kept coordination in Redis and truth in the database meant the durable state did not live in any worker that serverless would recycle. The poll-to-push inversion then deleted complexity rather than adding it: the custom autoscaler, the one-cluster-per-prefix rule, and the idle-scaling controller all fell away, replaced by the platform's native scale-to-zero.

None of the three hardening pushes that produced this shape — the reactive conversion, the move to statelessness, the modeling of the cross-service invariants — was aimed at serverless. Each was motivated on its own terms. Their convergence is the lesson: a system built reactive, stateless, and modeled is, almost by accident, a system that is safe to run serverless. The reactive seam was not a feature of the migration. It was its precondition.

Here is how fast the seam let the migration go — the operating loop the rest of the book describes. The timeline already tells the migration itself: a Monday teardown of an idle Kubernetes cluster, serverless by that night, about 400 commits structured into 27 phased designs. What matters here is the loop those phases ran: the agent proposes a phased design, it surfaces the decisions that need a human — one to eight judgment calls a phase — I make those calls, and it executes. It was a re-platforming that would be a quarters-long project in industry, run over two days because the seam had already been built right.

5.3.6 View 2 — the front end as model-view-controller over a shared edit language

The front end is a small single-page application plus a set of supporting surfaces — an account view, a job history, an operator dashboard, and the editor. The piece worth drawing is the editor, because it shows the cleanest decomposition. The editor is a model-view-controller loop over one document, drawn in Figure 5.3-3.

• The view is what the user sees: two panes. The left renders the page with overlay boxes marking each structural element; the right is a list of cards, one per element, with editable fields for alt text, role, decorative-or-not, and reading order.
• The controller takes a user gesture — edit this alt text, change this role, drag these children into a new order — and does one disciplined thing: rather than reaching into the document and mutating it, it translates the gesture into a single typed edit operation.
• The model is the document's intermediate representation. Its only input is an edit operation. It applies the operation, returns the updated state, and the view re-renders from that state.

The operation the controller emits is drawn from a small, closed vocabulary: set the alt text, set the role, mark an element decorative, reorder the reading order, set the document title, set the language, override the displayed text. That vocabulary is a little language for changing a document — an edit language. Every gesture routes through it for the reason that runs under the whole system: a document has exactly one way to be changed. The editor never edits the document. It speaks the edit language, and the model is the only thing that touches the document.

Learn more about this governance mechanism: closed edit-operation vocabulary.

The read-only diff views for slides and word processor files share this shape, differing only in the adapter that fetches their structure. One surface, one edit vocabulary, many formats. The uniformity is the payoff: a fix or a constraint applied to the edit language holds for every format and every producer that speaks it — and the more producers speak it, the more each fix is worth. This is the Modeling Thesis in miniature — a structured model binding what a change means to how the document is touched, so intent and implementation cannot drift apart.

5.3.7 View 3 — the edit language as the target of automated remediation

Here the two halves of the system join, and the join is the function-call pattern from earlier in the chapter, seen once more.

The edit language the editor speaks is not only the editor's. It is the same target the automated pipeline produces. When the pipeline decides a figure needs alt text, the result it emits is an edit operation — the very set-alt-text the editor would emit if a human did it by hand. The human path and the automated path are two producers of one language, and they flow into one document model that applies each operation and stamps it.

The mapping from a remediation task to an edit operation is a function: task in, operation out. And that function is a concrete instance of the LLM as a function call. Inside it, a bounded task — this figure, this context, this question — is packed into a typed input and handed to the model as a call; the model returns a candidate; and a deterministic validator checks the candidate before it is allowed to become an edit. The edit language is the typed output contract. An honest caveat: this task-to-edit function is mostly hardcoded today and will be fleshed out. What matters now is the shape and the trajectory, not a finished implementation — the concept is that automated remediation and hand editing are the same operation reached two ways. Figure 5.3-4 draws both paths into one edit language.

Why route through the language at all

The frontier models can already skip all of this. Opus and the project's own agent can take a slide deck and remediate it directly — at least for slides — with no pipeline, no edit language, no validator. So why build the machinery at all? Direct remediation buys neither of the two things a university needs. You cannot audit what a direct edit changed: the model hands back a file, not a list of typed changes you can inspect, explain, and reverse. And you cannot trust it: there is no deterministic check that the standard was met and the meaning survived. Routing every change through one edit language and one validated boundary buys both. Traceability comes free, because every edit is a typed, validated, stamped result with a history you can reconstruct. Confidence comes from the validator that sits at the trust boundary and refuses a candidate that fails.

There is a third dividend, and it connects this view to a habit the book returns to later. Scoping each model call to one bounded task also scopes the reasoning: the tighter the task, the less the model must reason over, and the fewer tokens the reasoning costs. A model asked to describe this figure under this context does less work than a model asked to remediate a whole document in one shot. That token-scoping is the same move as building the remediation as a series of small, bounded transformations rather than one giant leap — the same idea seen from the cost angle instead of the pipeline angle. A chain of scoped passes is cheaper to run and cheaper to reason about, because each link asks the model for exactly one small thing. (See: transformation — everything a model does well is a sized transformation, and sizing the leap is the skill.)

These three views were not drawn by hand. They were rendered from DocAble's real system models — typed records the fleet reasons through — and those models stay true to the code only because a traceability substrate re-checks them against it, the deep-dive we return to in the Model Zoo.

5.3.8 Same song, second verse

Notice the shape of the argument, because the book made it again at a larger scale. A model can do the one thing deterministic code cannot — look at a figure and understand it — and it is unreliable. You do not make it reliable by trusting it more. You make a reliable system by wrapping it: bound what you ask, type what comes back, validate before you believe. Inside DocAble, the wrapped component is a vision-language model writing alt text.

Zoom out one level and the coding agents that built DocAble are the same kind of component: powerful, probabilistic, capable of a confident wrong turn. The methods in the earlier chapters are the same pattern applied to them — bound the task, type the interface, validate before you trust. You have now seen, in the small, the pattern the rest of the book applied in the large. Same song, second verse.