3.1 The Executable Zoo

The previous chapter argued that a model is the sweet spot between prose too vague to enforce and code too verbose to reason over. It ended on a promise: this book would walk each kind of model on real code, with real invariants, and show how to keep the code from drifting away from them. This Part cashes that promise.

Recall the system behind all of this. There is a real codebase under every model that follows — DocAble, the production accessibility service this book runs on. It carries nineteen real, structured, drift-checked models and uses everything in this book to stay coherent. The full account is at the back, in The Built System — Part 5 (A MAGE Case Study).

The Executable Model Pattern

Everything after this chapter is one schema, worn five ways. Every executable model answers the same five questions:

• What engineering question does it let you settle that the raw code cannot?
• What invariant must hold?
• How is it derived, from the code or the code from it?
• How is that checked on every build?
• What drift does the check prevent?

Read the rest of Part 3 as instances of it.

3.1.1 Why models are newly central

Part 1 derived the Modeling Thesis from the machine. This Part earns it: here are the executable models themselves and the work each performs. Read as economics, the thesis runs three ways at once — agents need models (a raw codebase is too large for the window and too diffuse to reason over; the model is the compact representation the reasoner can hold), can maintain them (regeneration and reconciliation are the cheap, repeated cognition the substrate supplies — the next section prices this against the tradition that died for lack of it), and can enforce them (model-aware checks at the action and admission boundaries make a model a surface the build holds the code to, never advice).

Those three legs make a model more than a context optimization. One artifact serves as the agent's reasoning interface, the engineer's architectural specification, the generator's derivation source, and the build's assurance surface — four roles no prose document and no raw codebase can hold at once.

The architecture that delivers all four roles is the executable source-of-truth. The model is structured data. Agents read it to navigate and reason; generators consume it to emit the artifacts that must agree with it; drift gates block the build the moment code and model diverge. Every view in this Part is that one architecture, worn five ways.

3.1.2 The expense that buried MBSE is the one a fleet now pays cheaply

Model-based systems engineering never failed on its ideas. It failed on its upkeep. A model earns its keep only while it matches the code, and keeping a hand-drawn model matched to a moving codebase is human work — a person notices the code changed, finds the diagram it touched, and edits the diagram to agree. That labor is dull, unending, and the first thing a deadline cuts. So the diagrams drifted, then lied, then got ignored, and a discipline with sound ideas earned a reputation for ceremony that never paid its way.

The agent changes exactly that term. Re-inducing a model from the code, diffing it against the last version, regenerating the artifacts it feeds — this is the dull, unending work a fleet does for nearly nothing. The one expense that buried MBSE is the one thing an agent fleet supplies cheaply. A practice that never repaid its upkeep suddenly pays: the map stays equal to the territory because the recurring upkeep has moved off the human payroll. Someone still authors the model, the reconciliation rule, and the gate — what shrank is the standing maintenance, not the design. This chapter earns that claim: every model below is drift-checked on every build, not by a human who might forget.

The move now is to stop listing kinds of model and start walking them. The companion catalogue holds nineteen real, structured, drift-checked system-models — the actual embodiments of every kind the last chapter named. Reconciled with the general model types a systems-engineering course teaches, the zoo runs to twenty-nine named models. Treat that number as evidence rather than ambition; it grounds a single claim: the zoo is large enough that one model is never the whole picture, which is exactly Philippe Kruchten's thesis about architecture.

What admits a candidate to the zoo is the formal definition from The Agent Stack: a deliberately reduced, machine-readable representation of system intent, structure, behavior, policy, or evidence — one that supports reasoning, derivation, or checking, and is mechanically maintained against the system it represents. Registries, graphs, manifests, state machines, typed records: each earns the word the same way, by naming what it represents and carrying the gate that holds it true. A structure that fails a clause — a dashboard nothing derives from, a diagram nothing checks — stays out, however useful it is.

Scope, and where to read next. "Model-based systems engineering" here means software: the models are typed records, state machines, and the code's own structures, because the system the fleet reads and rewrites is pure software. Classical MBSE speaks SysML ¹1. Wikipedia, “Systems Modeling Language,” 2026, https://en.wikipedia.org/wiki/Systems_modeling_language. — blocks, constraint blocks, verify-and-satisfy traceability — a vocabulary these models quietly borrow, since a typed invariant with a pointer to the check that verifies it is a constraint block in all but the notation. What they refuse is SysML's usual form: a model drawn in a tool beside the code. That is a second representation of what the code already is, and a second representation is a snapshot — it drifts the moment the code moves, which is the very failure a derived model exists to kill. Borrow the words where they name something; keep the model bound to the code — derived in either direction, gated either way — not drawn alongside it. And it stops at discrete software: a system with continuous or real-time dynamics wants a different toolkit — the timed and hybrid automata of Alur and Dill ²2. Rajeev Alur and David L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science 126, no. 2 (1994): 183–235. (timed automata ³3. Wikipedia, “Timed Automaton,” 2026, https://en.wikipedia.org/wiki/Timed_automaton., hybrid systems ⁴4. Wikipedia, “Hybrid System,” 2026, https://en.wikipedia.org/wiki/Hybrid_system.) — out of scope here, and the place to read next if your system touches the physical world.

A larger claim starts here and pays off in the back matter. Working at the model level, with an agent doing the lifting, buys three things a team usually has to trade against each other: fewer tokens spent, more velocity, and higher quality — together, and without a corresponding cost. I did not model that claim; I lived it, as the preface already told. For the data, see The Timeline and the Work → The fewer-tokens leg is the Modeling Thesis paying rent: a model binds intent to implementation and shrinks what the agent must hold in-window to act on it, which is the book's answer to churn, the failure that limits an agent fleet. That combination is the shape of what Fred Brooks called a silver bullet, and Brooks argued no such thing exists. The careful version of the claim, defended in the implications, is that the model level is the closest thing to one, because it changes the representation the agent reasons over rather than promising to make the hard part easy. Each model page below is a small piece of the evidence.

Data from the case study

The fewer-tokens leg is the one we can measure directly. In a controlled A/B pilot, an agent answered four navigation questions about the modeled codebase — locate a component, trace an invariant, resolve a tier, find an anchor — once with the MBSE navigation guidance loaded (ON) and once without it (OFF), and we counted the tokens each arm spent to reach the answer. Table 3.1-1 reports the four tasks. For the data, see The Executable Zoo → (preliminary)

Preliminary — a controlled pilot (N=4 modeled navigation tasks; 2 placebo arms pending).

The median saving is about −35%, at zero accuracy loss — all four modeled arms answered correctly on both ON and OFF, so the guidance bought cheaper answers, not different ones. The biggest win (NAV-03) resolved a tier in one tool-call with guidance where the naive path took twenty-two, and that gap states the rule: the more derivation the naive path must redo, the more the guidance is worth.

3.1.3 Kruchten's 4+1, promoted from a closing sentence to the spine

The last chapter invoked Kruchten's 4+1 views in a final sentence — "the reason one model is never enough." This Part promotes that sentence to its organizing structure. Kruchten observed that no single diagram captures a software architecture, and that four complementary views plus a fifth that ties them together cover what a working engineer needs to see:

• The Logical view — the functional structure: the objects, the types, and how they relate. What the system is, as a designer sees it.
• The Process view — concurrency and synchronization: what runs at once, the locks, the runtime dynamics. What stays consistent under interleaving.
• The Development view — the module and organization structure: how the source is packaged, layered, and owned. How the code is arranged for the people and agents who build it.
• The Physical view — the mapping of software to hardware: where processes run, across which hosts and network boundaries. Where the parts live.
• The Scenarios view (the +1): the use cases and journeys that animate the other four and validate them. What the system does for someone, walked end to end.

One chapter of this Part takes each view. A reader leaves with four views seen built on real code, plus the scenarios that validate them — each view with its invariants and the checker that holds them true. Figure 3.1-1 draws the one trunk and its five views.

What this book adds to 4+1: the drift gate

Kruchten, of course, described the views; he did not have a drift gate. The drift gate is what this Part adds: every view here is not a diagram a human maintains but a structured model a tool reads on every build, with a gate that fails the build the moment the model and the code disagree. 4+1 tells you which views you need. The drift gate keeps each view from becoming a diagram that rots.

The framework is a choice; the core is not

Making the model executable is why this Part is not really about 4+1. Kruchten's five views are how this book organizes the zoo, because they map cleanly to an engineer's questions. But once the core is a structured model held equal to the code, the framework is a projection over that core, not a second thing you maintain. You keep one executable model and render whatever view-set the audience needs from it.

Change the audience and you change the projection; the model stays put. An engineer doing runtime analysis wants Kruchten's Process view. A customer asking "what are the moving parts, and what do you send my data through?" wants a C4 Context-and-Container view. A reader reasoning about invariants wants SysML's constraint-block vocabulary. A compliance reviewer wants a data-flow diagram. Rival methodologies, at first blush — yet each is a rendering of the same structure, and a system whose core is executable can derive any of them: the C4 view is the same projection move as the Process view, run over the physical/deployment model instead of the state machine.

The same move works one level finer. Even inside a single framework, a view must choose what to show: a customer's Container view hides the internal helper mesh a maintainer needs; a privacy review shows only the data stores and where they egress. That choice is a second projection, and it stays honest by a clean split. The content — which containers, edges, and external systems exist — is a pure function of the source models, authored by no one. The lens picks which of that content a view shows; it may hide a node, but it can never invent one. Name a container the sources no longer contain and the lens fails the same drift gate the view does, so even "the customer's slice" cannot drift from the truth. The word lens arrives with its theory attached. The programming-languages literature formalizes exactly this hide-but-never-invent contract as a well-behaved lens, one half of a bidirectional transformation ⁵5. J. Nathan Foster et al., “Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-Update Problem,” ACM Transactions on Programming Languages and Systems 29, no. 3 (2007): 17:1–17:65.; the drift gate checks at build time what the lens laws state as algebra. Figure 3.1-2 draws both projection axes — framework and lens.

What this Part teaches, then, is modeling in the general; 4+1 merely supplies the spine, chosen because it maps cleanly onto an engineer's questions, and each view gets built and drift-gated on real code. The transferable claim sits one level up: hit the executable core, and the framework wars dissolve into projection choices. Choose the core with care; choose the framework, and the lens, to fit the reader.

3.1.4 The trunk: machinery that holds any view true

Before the views, one chapter of framing. Most of the catalogue's method models do not belong to a single view. They are the machinery that makes every view executable and drift-proof, and rather than re-explain the drift gate in each view chapter, this chapter introduces it once and each later chapter revisits it.

• The executable source-of-truth. The pattern behind every view, named and defined at the top of this chapter.

Learn more about this governance mechanism: executable source-of-truth.

• The drift and parity gates. The lints and tests that enforce model-and-reality parity in both directions, so no model drifts unilaterally.

Learn more about this governance mechanism: drift and parity gates.

• The agent-first harness. Build the models as a thin hand-rolled layer over frozen records under a few disciplines: adopt the genre's schema, skip its heavyweight runtime.

Learn more about this governance mechanism: agent-first MBSE harness.

• The read and generate surfaces. One canonical query API over every model (read-don't-hardcode consumption), and generators that emit real artifacts from the models, each provenance-headed so a hand-edit is caught.

Learn more about this governance mechanism: model query surface.

These are the framing chapter's home. The view chapters name them again where each view's model reconnects to them. A few concepts have to land before the views begin: what an invariant is and how you write one, what model checking buys you, and what drift is. Each is introduced at the point it is first needed, and later chapters link back rather than repeat it.

Three beats frame the whole Part.

Beat 1 — a model is derived and joined, never repeated

The last chapter warned against repetition: two models that say the same thing must now be kept in sync. This Part sharpens that warning into the zoo's organizing rule. A model here is derived — from the code, or the code from it — never kept beside the code as a parallel document. And it joins to its neighbours on a shared key rather than restating them.

The service-flow model is the list the access policy is generated from and the call graph is checked against — it holds no second copy of the endpoints to re-list. The journey model joins to those endpoints by call-site rather than copying them. Repetition is the failure. Derivation and join are the cure. The flagship demonstration is the third worked example in the Scenarios chapter, where four models join so a journey's criticality reaches all the way to which host a test runs on, with no fact stated twice.

Beat 2 — name the direction of derivation

A model and the code it concerns stay equal by derivation, and derivation runs in one of two directions. Say which up front, because the machinery differs.

• Model-from-code (induce and reconcile). The code is authoritative; the model is a projection of it, reconciled at build time. The component-zone model reads the real directory tree; a journey's dependency list is derived from its real call sites. Here the drift gate is a reconciler: it re-induces the model from the code and fails on divergence. Reach for this when the code is the ground truth and the model is a compact, queryable view of it — the usual case for a large codebase an agent must operate.
• Model-to-code (specify and generate). The model is authoritative; the code, config, or docs are generated from it. The access policy, the service catalog, the wire-contract types are emitted from the service-flow model. Here the drift gate is a freshness and provenance check: the generated artifact carries a header, and a hand-edit or a stale regeneration is a finding. Reach for this when the model is the design intent and you want the artifact to obey it.

Most models in the zoo are model-from-code, because the codebase pre-existed the models. The service-flow model is the clearest model-to-code case, and it is bidirectional — some fields generated to code, others reconciled from it — which is why its gate checks both directions. Each model page names its direction.

Extracted Code Graphs and Intent-Bearing Models

The purest model-from-code artifact is not one of the zoo's own views. It is the repository graph a growing class of tools now hands a coding agent, so the agent stops rediscovering the codebase from raw files on every task. A parser walks the repository and records its entities and the relations among them: functions, classes, imports, calls, endpoints, schemas, tables, and the documentation links between them. The result is a persistent, queryable map. What calls this function? What depends on this module? Which path connects this endpoint to that table? What moves if this node changes?

That map earns its keep. It is richer than a flat symbol index and far cheaper to traverse than the whole tree. By the Modeling Thesis, that is the token argument already made for the zoo, pointed outward: the agent reasons through the derived graph instead of re-reading the code. Recent systems such as RepoGraph ⁶6. Siru Ouyang et al., “Repograph: Enhancing AI Software Engineering with Repository-Level Code Graph,” 2024, https://arxiv.org/abs/2410.14684., CodexGraph ⁷7. Xiangyan Liu et al., “Codexgraph: Bridging Large Language Models and Code Repositories via Code Graph Databases,” 2024, https://arxiv.org/abs/2408.03910., RANGER ⁸8. Pratik Shah et al., “RANGER: Repository-Level Agent for Graph-Enhanced Retrieval,” 2025, https://arxiv.org/abs/2509.25257., and Codebase-Memory ⁹9. Martin Vogel et al., “Codebase-Memory: Tree-Sitter-Based Knowledge Graphs for LLM Code Exploration via Mcp,” 2026, https://arxiv.org/abs/2603.27277. derive such graphs for navigation, dependency traversal, and agent retrieval; Codebase-Memory reports roughly a tenfold reduction in tokens and 2.1 times fewer tool calls against a file-exploration agent, at some cost in answer quality (83 percent against 92). These systems give an agent an increasingly capable model of the artifact. MAGE's separate concern is how that descriptive structure joins to authored intent and mechanically enforced policy.

Here is where the join bites. An extracted graph describes what exists. It can show that component A calls component B. Extraction alone cannot say whether A is permitted to call B, whether B owns that responsibility, which user goal the edge serves, or what invariant the call must preserve. None of those are syntactic facts waiting in the artifact to be recovered. An engineer decided them.

Beat 2 named one axis: which artifact is authoritative, code or model. Lay a second axis across it. Not how the representation was made, but what claims it is authorized to make. A descriptive model recovers the territory. An intent-bearing model states the shape the territory is meant to have. The first is built to navigate and to estimate impact. The second is where specification, prediction, and governance live.

The boundary bends both ways. A MAGE model may begin as an induced description of existing code, and a code graph may fold in documentation, schemas, or inferred clusters. So provenance is not the question. Authority is. Does the representation report that an edge exists, or declare the edge permitted? Does it list the running services, or name which service owns a capability? Does it record observed behavior, or define the transitions the system is allowed to make?

Put that way, the two kinds of model compose rather than compete. A code graph finds every caller of a raw PDF library. An authored architecture model declares that a single structured model owns mutation of that format. A gate compares the extracted callers against the permitted set and turns any extra edge into a build finding. The graph supplies the current fact, the authored model supplies the policy, and the gate reads one against the other. This is the same drift check the zoo runs everywhere, now with a descriptive map on one side and a normative model on the other.

That composition is a governed engineering environment in miniature, and it settles where these tools sit. A code knowledge graph is a strong input to MAGE: it can serve the observed-reality side of any drift or parity gate. What it does not carry by itself is the ought. The Modeling Thesis puts both representations in front of the reasoner, the map of what is and the model of what should be. The Alignment Thesis keeps the descriptive map, the intended design, and the running code from drifting apart in silence.

A shorthand, offered as a center of gravity and not a fence: a code knowledge graph compresses implementation; a MAGE model compresses engineering meaning. Both are models. Both can be induced. Both help an agent reason. What MAGE requires past the graph is a place for the ought, and a mechanism that holds the is against it.

The ought can also be authored a simpler way: by writing it down. Spec-driven development gives every meaningful feature a written specification before any code, and has agents implement against it, the spec standing as a contract between intent and code. It is a real move toward authored intent, the same normative commitment MAGE makes, and it holds until the corpus grows. Recent studies of spec-driven agent workflows converge on the same normative point: an industrial one-person-squad case that ran an explicit spec-driven process to deliver work scoped for a four-person team reports that specification quality and institutional knowledge — not raw model capability — decided the outcome ¹⁰10. Marcelo Vilas Boas et al., “One Developer Is All You Need: A Case Study of an AI-Augmented One-Person Squad in a Brownfield Enterprise,” 2026.. One team's field report is exact about where it broke ¹¹11. Abdurrahman, “We Adopted Spec-Driven Development, Then the Specs Started Eating Our Context Window,” Medium, July 2026, https://abdurrahman5.medium.com/we-adopted-spec-driven-development-then-the-specs-started-eating-our-context-window-6cb9476dfedc.. Their naive preload reached roughly thirty-five thousand tokens at startup, of which about six percent was relevant, and the agent degraded once the window passed half full. Size was not the worst of it. A specification the code had moved past produced "syntactically correct code that was wrong," because the agent trusted it. "A stale spec is worse than no spec, because the agent trusts it."

Read against the two theses, that report is convergent evidence, not a rival. Its remedies climb the same hill this chapter has been climbing. Living specs, one per feature and edited in place, are the derive-don't-snapshot rule under another name. A thin router and index that load only the matching documents reach for a context-management layer, the answer to loading the right small slice instead of the whole corpus. Generated wikis and a CI check that flags a doc-against-code mismatch are a drift gate and derived traceability, bolted onto a prose corpus after the fact.

The difference is representation. A spec states the ought in prose, which does not compress and drifts unseen. A structured model states it in a form the machine reads: the right slice is small by construction, so the reasoner reasons through the model rather than through tens of thousands of tokens hoping the relevant fraction lands; and a gate holds the model against the code, so it cannot go stale-but-trusted, the failure the report names most sharply. The remedies spec-driven development reaches for by hand are first-class here.

So three ways to hand a fleet a system it can reason about fall on one axis. A code knowledge graph recovers what the code is. A spec writes down what it should be, in prose the agent must re-read and can outrun. A structured model states that same ought where a compiler and a gate can hold it to the code. Only the last keeps intent both compact and true.

Beat 3 — every model traces to the code

A model earns trust only if you can get from a model element back to the lines that realize it, and forward from a line to the model element that governs it. That round-trip is traceability. It is exactly what the safety-critical standards demanded and exactly what the drift gate mechanizes: the reconciler is a traceability check that runs on every build. The forward direction is itself measurable — how much of the tested code reaches any model — and driving that number up is how the case study drained its unmodelled code. For the data, see Metrics → (preliminary)

Traceability is why the per-model template folds a one-line note into each page — the direction the model derives, and the join key from a model row back to the code. A reader always knows how to round-trip from the picture to the lines.

The round-trip is also what the whole zoo rests on. A set of views earns trust only while every view still tracks the code it depicts; the moment one describes a subsystem the code has retired, it misleads every agent that reasons through it. A zoo of drifted views is worse than none, because it lends false confidence. Kruchten gave the reader four views and a fifth to validate them. He did not say how a view stays equal to the code once both have hundreds of authors and a fleet rewriting the territory daily.

The answer this book defends is that the round-trip must itself be derived, not snapshotted. Picture the graph it walks — model element to lint to code entry point to test to registry row, each hop an edge. Write those edges down once and trust them, and the graph is a frozen snapshot that drifts the first time a symbol it names is deleted. Give each edge the mechanism that re-proves it — resolve the target against the code and see whether it still exists — and a deletion turns the edge red. A check that re-reads the code cannot fall behind it; a stored copy can.

The graph pays a second dividend. Because a resolving edge means the map is current, an agent can walk it to pull the slice of a codebase it cannot hold in one window — up from a line to the invariant that governs it, down to the code that realizes it. The systems model a senior engineer keeps in their head becomes a navigable index the fleet reasons through. Drift-detection and navigation are one property wearing two faces: an edge that resolves is both a true claim and a current map. The next section reads the concrete mechanism off DocAble's real drift; the catalogue carries it as its own entry.

Learn more about this governance mechanism: symbol-anchored traceability graph.

3.1.5 Keeping the models honest — the traceability substrate

DocAble did not design this up front. It tried the cheaper approach first, watched it fail on real work, and built the machinery from what broke. The story is worth walking, because it shows the exact shape a snapshot rots into and why a derived edge does not.

A model is only as good as its agreement with the code. Say a model still describes a poll-based dispatch plane after a serverless push plane replaced it — DocAble's real mid-project migration — and every agent that trusts the model plans against a system that no longer exists. The map has to equal the territory, or the map lies.

The tempting way to keep them equal is a checklist: when you retire a subsystem, remember to update the model too. DocAble tried that and it failed the way it always fails. A cutover retired the poll plane, the retirement doc dutifully reconciled the architecture docs and the agent boot context, and it forgot the models. The forgotten edge stayed green because nothing re-checked it. That is the pattern under every silent drift: a hand-maintained list rots the moment the code moves without it, and no one notices until the stale fact bites.

Reading the fix off real drift

The right sensor was read off real drift rather than guessed. The models were left deliberately ungoverned for weeks and the fleet allowed to drift them, so the fix could come from observed failure instead of imagination. An audit of the closed work — every job green at its own done-check — turned up two dozen silent divergences at a signal-to-noise near one. A checker tightened past the producer it now rejected; a typed function shipped and wired to nothing; a reconciliation lint gone red the instant its work closed. Sort those cases by what caught them and one line separates the clean from the drifted. The clean ones had a sensor that re-read the code at check time. The drifted ones kept a second copy of the fact, maintained by hand, that fell behind.

So DocAble keeps a traceability graph in place of a checklist, and every edge in it is derived — re-checked against the code at scan time rather than trusted from the last time someone looked. The nodes are things the system already has: a model element, the lint that enforces it, the code entry point that realizes it, the test that verifies it, a registry row, a doc surface. The edges are the joins between them — this invariant governs that code root, that test verifies this invariant. Each edge carries the mechanism that re-proves it: run the resolver against the target and see whether the symbol still exists.

Two decisions that make the graph resist rot

• Anchor to symbols, never to line numbers. An edge points at a function or class definition, resolved statically — not at a file-and-line. Line numbers churn under every edit above them; a symbol survives every edit that does not delete it. When five journey anchors drifted stale under a refactor, the cause was line-anchoring. A symbol anchor moves with the code it names.
• A missing symbol is a finding, not a crash. When an edge points at a symbol that no longer resolves — deleted, renamed, moved out — the edge goes red, and that red is the drift becoming visible. The sharper case: when the model wants to point at logic for which no clean symbol exists, buried in a god-function, the absence signals the code is missing an abstraction the model needs. The anchor doubles as a probe for where the code is under-factored.

The sensor that walks the graph runs at a slower cadence than the per-commit gates, on purpose. Resolving a symbol against the code — a jedi or Roslyn round-trip per anchor — costs far more than the cheap membership lookups a commit hook can afford, and the costlier the check, the slower the cadence it earns: the derived-edge check fires at review and done-checking time, not on every commit. A second, cheaper guard sits on the anchors themselves, watching for the case a symbol walk cannot catch — a pointer left naming a dead implementation while a replacement was built beside it. That pointer-drift guard was earned by the most expensive drift of the build, a retired deploy-orchestration script whose stale pointers still named a dead implementation and fired a prod-blocking deploy.

This is the same commitment as the one structured model under every format, one level up. There, a fix applied through the model holds for every format because there is exactly one place to apply it. Here, a model stays true to the code because the join between them is re-derived, not remembered. In the system that underpins this book, the audit's line held without exception: derived sensors defended; snapshotted ones drifted. A sensor that reads the source of truth at check time cannot fall behind it. A hand-maintained copy of the same fact always can.

3.1.6 How to read a model page

Every model in this Part is rendered by filling the same five-field template. The uniformity is deliberate: a reader who has read one page can read any of them on reflex.

• (a) Quality property it helps assess. The property this model lets you check — stated as the question the model answers that the raw code cannot. Not "it models X" but "it lets you ask, and answer, is Q true?" A model with no quality property to assess is a diagram, not a model.
• (b) Constructs and relations. The typed elements the model is built from and how they relate — the record kinds, the fields that carry meaning, the edges between them. ^** The modeling tradition calls this field the model's metamodel, and names the full layering M0–M3: running instance, model, metamodel, meta-metamodel, bottom to top. We keep the layer and skip the tower — a frozen record schema is metamodel enough, and the host language's type system stands in for M3. The MDSE text (Brambilla, Cabot, and Wimmer, ch. 2) draws the tower in full. This is the reference content: what a reader consults to understand the model's shape.
• (c) Visual depiction. The diagram of the real model, matched to its natural type — a state machine gets a state diagram, a topology gets a deployment diagram, a registry of related records gets an ER diagram. Each carries an accessible description that states the content and the takeaway.
• (d) Invariants, and how they are checked. The predicates that must hold, each with the mechanism that holds it true — a drift lint, a coverage floor, a model check, a parity gate. Rendered as a table of invariant, its temporal shape, and how it is checked. A model whose invariants are prose with no checker is flagged UNTESTED.
• (e) Traceability and derivation direction. One line: which direction the model derives, and the join key from a model element back to the code.

The first four fields map onto the four questions a reader brings to a model: what is it for, what is it made of, what does it look like, how do I trust it. Field (e) answers the fifth this chapter raised: how does the model stay tied to the code. Each view chapter opens with the Kruchten view it embodies, then walks its models through this template.

3.1.7 The coherence triangle

Every model page in this Part draws the same shape. Fields (b) and (c) give the structured model: records, edges, state machines. Field (d) adds the invariants, the predicates that must hold, each named by a stable id. Its checker supplies the coherence-gate: the drift lint or model check that holds a predicate true at build time. Model, invariants, gate — the constraint-and-verify vocabulary the chapter already borrowed from SysML, where a constraint block wires to the check that satisfies it.

The model provides two kinds of value. First, the schema — records, edges, state machines — names the parts and gives the tools something to read. Second, the invariants that get checked: the predicates that must hold. Value both. The triangle's point is that the invariants and their gate complete the model's value, not that the schema earns nothing. A structure that names its parts but promises nothing you can test is only half a model; field (a) drew that line, and field (d) stamps an unchecked invariant UNTESTED. Draw the schema and stop, and it rots the first time the code moves past it. The gate keeps it honest.

The invariants are not arbitrary. They come from the failures the system met. In the DocAble build, the gaps the models caught were violated-but-unstated invariants — a property the system had always needed and never written down, promoted to a checked predicate the moment it broke. Part 5 records the act behind each one: deciding, for every failure, whether it was a one-off to patch or the symptom of a missing mechanism. Promoting the property to a checked invariant is what makes the model the right abstraction, not merely a plausible one. Figure 3.1-3 draws the three nodes and the edge that closes them.

---

What is an invariant, and how do you write one?

An invariant is a statement that must be true in every state your system can reach — a property the system promises never to violate. You write one as a predicate over the model's state, then you ask the model whether any reachable state breaks it. Take a job that can be free, leased, or done. The invariant "a job is never both leased and free" is a predicate over one state: not (leased and free). Because it concerns a single state, you check it by visiting every reachable state and evaluating the predicate there. If none breaks it, the invariant holds. The move that makes this more than a comment: the predicate is checked, exhaustively, by a tool, not eyeballed on a diagram. That is the step from "we believe this holds" to "we proved it holds."

STATES = {"free", "leased", "done"}
def invariant(state): return not (state == "leased" and state == "free")   # never both
assert all(invariant(s) for s in reachable_states())   # check every reachable state

Derivation direction, boxed for reference

Two directions, from Beat 2. Model-from-code: the code is authoritative, the model is a projection reconciled from it, and the gate re-induces the model and fails on divergence. Model-to-code: the model is authoritative, the code or config is generated from it, and the gate is a freshness-plus-provenance check that catches a hand-edit or a stale regeneration. Reach for model-from-code when a large codebase pre-exists the model; reach for model-to-code when the model is the design intent you want the artifact to obey. A model can be both at once, on different fields.

What is drift, and what is a drift gate?

Drift is the condition where a model and the code it describes disagree — the map no longer matches the territory. A human-maintained diagram drifts silently the first time a developer changes the code and forgets the diagram. A drift gate is the build-time check that set-diffs the model against reality in both directions and fails the build on any divergence. Model ⊆ reality catches a model element with no code behind it; reality ⊆ model catches code the model never declared. Because the gate runs on every build, drift cannot accumulate: the first divergent commit fails, not the fiftieth. This is what makes an executable model different from a diagram — the diagram can drift, the gated model cannot.

The remaining insets appear in the view chapters where they are first needed: assertions over sequences and the temporal-logic step-up, bounded model checking, automata, data-flow diagrams, safety versus liveness, protocols and TLA+, and coverage over model nodes.

That is the trunk. The rest of this Part is the branches. This chapter built the shared machinery — the executable source of truth, the drift gate that fails the build the moment model and code diverge, the derived edges that keep the map equal to the territory — and set the admission test and the five-field template every model below obeys. What remains is to walk the five views on real code, each with its invariants and the checker that holds them true. The Logical view is first: what the system is.