Part 2 — Modeling  ::  Chapter 12

2.8 System Knowledge: Connecting the Models

The six preceding chapters each drew a different model of the same product. It would be natural to read them as six views onto one large model that holds structure, behavior, ownership, policy, measurement, and provenance together. DocAble has no such model, and MAGE requires none. Instead, the system uses a family of structured models, each built for a different question. Shared identity and traceability connect them where engineers repeatedly need to relate one view to another. System knowledge is not a seventh class of model. It is the substrate that lets the six classes work as a system.

2.8.1 A Heterogeneous Modeling Substrate

DocAble's models differ in shape on purpose. Some are registries of components and their relations. Some represent state transitions. Some encode contracts or decisions. Some capture quantitative relationships. They share identities, derivations, query surfaces, and traceability where those help, but nothing forces them into a single representation. Read the collection as a modeling substrate, not as one system-knowledge graph.

The substrate is concrete, and it is larger than any one chapter. In DocAble it holds on the order of ninety structured model modules plus several data dialects, organized in layers: a component-identity layer names what exists; a per-component metadata layer annotates each one; orthogonal meta-files sit across the top for deployment topology, inter-service edges, data flow, required environment, state machines, and the governance graph itself. In DocAble, these models are represented as data rather than importing the implementation they describe. This keeps model and territory separable enough for correspondence to be checked. When a model is meant to provide independent evidence of correspondence, keep it distinguishable from the artifact it checks. Figure 2.8-1 abstracts this substrate to the six model classes and the shared identities that join them.

Heterogeneous models arranged as peers around shared identities A radial arrangement. At the center sit shared identities. Six purpose models — structural, behavioral, ownership, decision, measurement, and provenance — are peers around the center, each joined to it. No model sits above another. Traceability, derivation, and query surfaces surround them in a footer band, not inside the identity center. The unity is semantic, not a hierarchy. DOCABLE MODELING SUBSTRATE · SIX PEER MODELS SHARED IDENTITIES structural behavioral ownership decision measurement provenance traceability · derivation · query surfaces Six peer models joined through shared identities — no tiers, no single universal graph.
Figure 2.8-1. Heterogeneous models over shared identities. Structural, behavioral, ownership, decision, measurement, and provenance models remain separate representations while joining through stable identities and explicit correspondence where needed.

The unity that matters is semantic, not syntactic. A service named in a structural registry is the same service a flow model references. A work item in an ownership view resolves to the lifecycle and the measurements for that work. A provenance event identifies the operation whose effect it records. Nothing demands that the models share a file format or metamodel; they need only agree on entity identity.

That agreement follows one discipline: prefer shared identity and derivation over independently maintained copies of the same fact. Where one model needs a fact owned elsewhere, join through a stable identity or derive a projection. For example, the access policy is generated from the service-flow model rather than maintaining a second endpoint list; a journey model joins to those endpoints by call site rather than copying them. Where duplication is unavoidable, make the correspondence explicit and checkable. This reduces the number of independent truths that must be reconciled by hand.

Static and runtime representations need not collapse into one model either. A computation graph can identify a remediation pass and its declared relations while a provenance record identifies the mutations realized during one run. When engineers repeatedly need to relate the two, shared identity can join them. One such question: which modeled computation produced this mutation? Where no such question pays for the join, they stay separate. In DocAble that particular join is deliberately not yet modeled: the representations remain orthogonal until a question makes their relationship worth the cost.

Shared identity also provides a query entry point. An agent — or an engineer — enters the substrate through the object its task names and traverses outward, following identities across models rather than loading everything. A canonical query surface lets the agent traverse represented relationships rather than rediscover them through repository search: name a component and ask what it owns, what it depends on, which flow reaches it, what its lifecycle looks like. The agent does not need the whole model. It needs the connected slice that answers the engineering question in front of it. Figure 2.8-2 draws that entry and outward walk.

Task-driven traversal: enter at a named entity, follow only the relations needed A task enters the substrate through a named system entity, shown by an arrow into the entity. From the entity, six model relations fan outward as peers: structural, behavioral, decision, measurement, provenance, and ownership. There is no order among them. The task retrieves only the relations its engineering question requires. TASK enters at a named entity named ENTITY e.g. a job, a service decision behavioral structural ownership provenance measurement Retrieve only the relations needed for the current question. No order among the six — enter at the entity, follow what the question needs.
Figure 2.8-2. Task-driven traversal. A task enters the substrate through a named system entity and follows only the model relations required by its engineering question.

2.8.2 Maintain Explicit Correspondence

Multiple models create a correspondence problem: represented facts can diverge from the system or from one another. Engineer the relationship between map and territory so divergence is caught rather than assumed away. Which machinery you reach for depends on which side is the source of truth.

Make the direction of correspondence explicit. Where the implementation is the source of truth, derive the model. Where the model is the source of truth, generate the downstream artifact. Where neither fully determines the other, maintain traceability and check the mechanically decidable correspondences. Figure 2.8-3 lays the three cases side by side.

Derive when implementation owns the truth

The model is a projection of the code, reconciled at build time. A component-zone registry reads the real directory tree; a journey's dependency list is induced from its real call sites. The drift check is a reconciler — it re-derives the model from the code and fails on divergence. This pattern is common when models are introduced into an existing codebase. ### Generate when the model owns the truth

Code, configuration, or documentation are emitted from the model. The access policy, the service catalog, and the wire-contract types are generated from the service-flow model. The drift check is a freshness and provenance check — the generated artifact carries a header, and a hand-edit or a stale regeneration is a finding.

Three correspondence patterns: derive, generate, trace and check Three panels. Derive: implementation in gray flows up to a model in blue, when the implementation is the source of truth. Generate: a model in blue projects down to implementation or config in gray, when the model is the source of truth. Trace and check: a model and system are linked two ways with a rust check, when neither fully determines the other; only the decidable correspondences are checked. DERIVE implementation is source of truth implementation derive model GENERATE model is source of truth model generate implementation / config TRACE + CHECK neither fully determines the other model check (decidable) system Three correspondence patterns — derive where implementation leads, generate where the model leads, trace and check where neither does.
Figure 2.8-3. Three correspondence patterns. Derive where implementation is the source of truth; generate where the model is the source of truth; otherwise maintain traceability and check the correspondences that are decidable.

The remediation computation graph is DocAble's fullest instance of the derive case, for both nodes and edges. Registered passes supply the computational entities. Each PDF pass also declares its typed Produces, Consumes, and ConsumesForControl facets, and the graph projects its structural relations from those declarations: nodes projected from the registered computations, edges projected from the typed composition. Change a pass's declared IO and the projected edge set changes with it. No second, hand-maintained list of data-flow edges sits beside the code waiting to fall behind, and a blocking parity check fails if the projection and the declarations disagree.

The graph is derived, but it remains a model: it suppresses method bodies, internal algorithms, runtime history, timing, and most document state, keeping only the entities and relations its structural questions need. Derivation prevents one kind of drift by construction, since an engineer never authors the edges, but it does not establish that the underlying architecture is good, nor that the declared relations capture every obligation that matters. Those are separate claims, and Part III separates them.

Trace and check where neither owns the truth

Where neither side can be fully derived from the other, the move is traceability plus drift checking. Relate each model element to the implementation that realizes it, then check the correspondences a machine can decide. Keep that relation live: resolve the target against current code when the check runs, rather than storing a line number or a symbol name that is itself another snapshot able to drift. A deleted target then surfaces as a finding instead of a stale green edge. In DocAble a traceability gate resolves each model-to-code anchor through a language-aware resolver — one for each source language — and reports every anchor that no longer resolves. Before the gate existed, such renames could silently strand model references.

Some correspondence remains semantic

Mechanical correspondence has a declared surface. Some claims are decidable: an anchor resolves, an observed dependency belongs to the permitted set, or a generated artifact is current. Other claims remain semantic and require judgment. Still others are not modeled at all.

These are different gaps: a semantic miss occurs when correspondence still holds syntactically but meaning has changed; an unmodeled region has no model-based coverage. A recurring miss is a candidate for refining the representation or adding a control. Figure 2.8-4 distinguishes mechanically decidable claims, semantic claims requiring judgment, and properties outside the modeled surface.

Coverage of model correspondence: modeled surface and unmodeled surface Two surfaces. The modeled surface splits into decidable claims, which get a mechanical check, and semantic claims, which need judgment. The unmodeled surface has no model-based coverage. A small arrow notes that a recurring miss should refine the representation or a control. Coverage of model correspondence MODELED SURFACE decidable claims →  mechanical check semantic claims →  judgment UNMODELED SURFACE no model-based coverage recurring miss → refine representation / control Mechanical checks reach only what the representation makes decidable; semantic claims need judgment, and unmodeled properties have no coverage.
Figure 2.8-4. Coverage of model correspondence. Mechanical checks cover only claims the representation makes decidable; semantic claims still require judgment, and unmodeled properties have no model-based coverage.

For invariant-bearing models, one useful executable pattern is a structured schema plus checked predicates over that schema. The schema defines entities, relations, fields, or states; the predicates state properties that a checker evaluates over the declared domain. Other executable models may instead drive generation, simulation, transformation, or analysis. A schema alone does not establish correspondence to a changing system; checks or derivations are needed where that correspondence matters. Figure 2.8-5 draws that relationship.

Checked predicates over a structured model: model, invariants, checker A linear pipeline. A structured model of records, edges, and states supports predicates over its domain. Those predicates are invariants, each with a stable id and a declared domain, for example the lease invariant leased if and only if an owner exists. A checker — a model check, a drift lint, or a validator — evaluates them. A side arrow shows that a recurring failure yields a new or refined invariant. This is one executable-model pattern, not the definition of executability. STRUCTURED MODEL records · edges · states a job: free / leased / done INVARIANTS stable ids + declared domains leased ⇔ owner exists CHECKER model check · drift lint · validator supports predicates over evaluated by recurring failure → new / refined invariant
Figure 2.8-5. Checked predicates over a structured model. A structured model supplies the domain; invariants state properties over that domain; a checker evaluates them at a declared cadence. This is one executable-model pattern, not the definition of executability.
FORMAL METHODS

Inset — What is an invariant?

An invariant is a property required to hold over a declared domain of states, structures, or observations. In a behavioral state machine, the invariant may be a predicate that must hold in every reachable state; in a structural model, it may require every observed dependency to belong to a declared set; in a measurement model, it may require a quantity to remain within a hard capacity bound. State both the property and the domain the checker claims to establish it over.

Take a behavioral illustration. A job carries two fields at once — a status of free, leased, or done, and a lease_owner that names the holding worker or is empty. Different steps write the two fields, so they can fall out of agreement, which is exactly why you write the invariant down. "A job is leased if and only if it has an owner" is a predicate over the pair: (status == "leased") == (lease_owner is not None). A free status with a lingering lease_owner is a stale lease; a leased status with no owner is a lost lease. Separating the two writes can make either inconsistent state reachable, and both break the predicate. The predicate becomes mechanically meaningful when a checker evaluates it over the declared reachable state space:

STATES = product({"free", "leased", "done"}, {None, "worker-1", "worker-2"})
def invariant(s):                                    # leased iff owned
    return (s.status == "leased") == (s.lease_owner is not None)
assert all(invariant(s) for s in reachable_states())  # check every reachable state

None of this proves the model right. Synchronization does not establish that the model is correct. A model can be structurally in sync and still express the wrong architecture. A pointer can resolve while its meaning has changed. A schema and its generated client can agree while a live producer emits something else. The guarantee the machinery offers is narrower, and worth stating plainly:

For the surface the model claims, check the correspondence that can actually be decided.

That boundary returns in Part III, where correspondence and correctness part company. Derive where implementation is the source of truth; generate where the model is the source of truth; trace and check where neither fully determines the other.

2.8.3 Modeling Makes Properties Available to Alignment

A model does not govern the system merely by existing. The structural model can name a forbidden dependency without preventing it. The recovery model can name an illegal transition without rejecting it. The measurement model can represent a budget without stopping the work that exceeds it. The provenance model can specify the evidence an operation should leave without requiring the operation to leave it. Each class makes a property explicit; none, by itself, gives that property force.

The remediation graph makes the point concrete. Its projection supplied a structural property, and its parity check supplied correspondence evidence, yet neither settles whether the represented architecture is itself correct. Part III separates that correspondence obligation from the question of whether the architecture itself is correct. A blocking parity check therefore establishes correspondence, not conformance.

Modeling makes an engineering property explicit; Alignment gives selected properties consequence. Where an appropriate boundary and evaluator exist, a constraint may exclude an unwanted state, a sensor may produce relevant evidence, a validator may evaluate it, and a gate may give the verdict consequence. Figure 2.8-6 draws the path from territory to consequence.

Modeling makes properties available to Alignment — but is not the only path Two paths join at one Alignment. The direct path: a territory or action is acted on directly, a local observable obligation. The model-mediated path: territory is reduced by abstraction to a model, which makes an explicit property available, a richer semantic obligation. Both land side by side on one Alignment — constraint, sensor, validator, gate — which leads to consequence. Governance can act directly; models add reach but are not required. Two paths to Alignment DIRECT PATH TERRITORY / ACTION a test, a diff, a sandbox run acted on directly local observable obligation MODEL-MEDIATED PATH TERRITORY abstraction MODEL makes explicit EXPLICIT PROPERTY available to richer semantic obligation ALIGNMENT constraint · sensor · validator · gate gives consequence CONSEQUENCE Alignment mechanisms can act directly on observable actions; explicit models make richer system properties available too — model-mediated is not the only path.
Figure 2.8-6. Modeling expands the semantic reach of Alignment. Alignment mechanisms can act directly on observable actions and artifacts; explicit models make additional system-level properties available for constraint, sensing, evaluation, and admission.

As a model makes more system semantics explicit, more system-level obligations become available for analysis and governance. A local static check can constrain a local, syntactic property with almost no explicit modeling. Architectural boundaries, temporal obligations, distributed ownership, provenance requirements, and end-to-end policies each require a representation that exposes enough system semantics for the obligation to be evaluated.

Modeling can therefore make an engineering tolerance explicit: it can state which variation the system may admit and which variation would violate an obligation. It can also leave the remaining realization choices visibly open. Neither fact gives the model authority. A represented boundary may remain advisory, just as an unrepresented local rule may already be enforced by a type, sandbox, or test. Part III asks the next question: which obligations should the environment itself hold, and what evidence and mechanism are sufficient to give them consequence?

Alignment does not require a separately represented model. A sandbox can deny network access, a compiler can reject an illegal construct, and a test can block a regression over observed behavior. These mechanisms already carry real authority.

Models expand the semantic reach of such authority. By making architecture, behavior, ownership, decisions, measurements, and provenance explicit, they make properties available that would otherwise have to be reconstructed by a human or agent each time.

Models can provide value before enforcement: they support reasoning, analysis, composition, and traceability. Part III asks the separate question of authority—what obligations the environment should hold, where they become decidable, and which mechanisms should give them consequence.

© James C. Davis, 2026–present