Appendix B - 19. Symbol-anchored traceability graph (derived edges)
The Structure of Symbol-anchored traceability graph (derived edges) — its shape at a glance:
Projected from the catalogue entry system-models / Symbol-anchored traceability graph (derived edges).
On this page: Intent · Motivation · Applicability · Structure · Sample Code · Consequences · Example use within DocAble · Related Patterns
Intent
Intent — Link every model to its lint, its code entry-point, its proof, its related models, and its registry as a typed graph whose every edge is a derived obligation a lint re-checks — each edge terminating on a resolvable symbol, never a line number — so when the code moves and breaks an edge, the model↔code drift becomes mechanically visible at scan time. The governing principle: derived edges defend; snapshotted ones drift.
Motivation
The executable models that let a context-bounded agent operate a context-exceeding codebase are only useful while the map equals the territory. But a model states more than facts about itself: it names the lint that enforces it, the code root it governs, the test that verifies it, the registry it reconciles against. Those cross-references are the joins an agent walks to jump between levels of abstraction — and they rot the moment the code moves without them.
The failure is silent traceability rot. A model's reference to a code symbol goes stale when the symbol is deleted, renamed, or moved, and nothing notices — the model still looks authoritative while pointing at a ghost. It recurs on every refactor that touches a referenced symbol: a deleted enforcement routine, a checker that was made stricter without a matching edge to the producer it now rejects, a "which implementation is live" pointer left aimed at a retired one. Each stale edge is a lie the fleet reads as truth, and the blow-up lands days later in a downstream gate instead of at the change that caused it.
The design was not guessed. The models were left deliberately ungoverned after creation and the fleet allowed to drift them, so the mechanisms could be designed from real observed drift instead of a hypothesis. An exhaustive audit of recently-closed work — each with a green definition-of-done at close — harvested roughly two dozen drift instances at a signal-to-noise ratio near one and zero false positives: a checker made stricter than the producer it now rejects, a subsystem retired from the code but still present-tense in the model, a fully typed function wired to zero production consumers, a reconciliation lint gone red the moment its Epic closed. That corpus is what "derived defends, snapshotted drifts" was read off of, not asserted into — the clean cases all had a mechanism that read the source of truth at check time; the drifted ones all had a parallel hand-maintained list that rotted.
Applicability
- Static symbol resolvers already exist — a language-aware analyzer per code language whose cross-reference the graph composes, rather than a new resolution engine. The graph is a typed view over resolvers that already ship.
- Typed models with addressable elements — the nodes the edges terminate on (model invariants, lints, code roots, tests, registry rows) are first-class, citable things.
- A place for the edge to live in-situ — the anchor rides with the code or model site (a typed reference field, a structured comment trailer) so it travels when the symbol moves, read by a derived lint rather than held in a central snapshot.
- A criticality/cadence policy — because re-derivation is costly, a declared rule for when it runs (audit / definition-of-done, not per-commit) so the cost lands where it earns its keep.
Structure
The Structure diagram appears at the top of this page.
Sample Code
Consequences
- Resolution is expensive, so the check is not per-commit. A cross-reference per symbol over a large tree is slow; the re-derivation lint is a scan-time / definition-of-done mechanism, and a fast keyword companion catches the cheap cases inline. Force it per-commit and it taxes every change.
- A weak-prover fallback is a standing ⚠️. A code anchor that resolves only by textual presence is a declared weak edge the coverage view surfaces; left un-burned-down it re-admits the drift the strong prover exists to remove.
- Resolution catches deletion, not demotion. A symbol that still exists but no longer plays the role the edge claims resolves green. The keyword companion (present-tense role-currency) covers that gap; the two are complementary, and treating one as subsuming the other leaves a blind spot.
- The edge vocabulary must fit the domain. A relationship the closed kind set can't express forces an enum change — the honest signal that the join web grew a dimension, not a reason to smuggle in an untyped string edge.
Example use within DocAble
- A traceability graph over the system models whose typed edges join each model element to its enforcing lint, its governed code root, its verifying test or formal proof, its related models, and its registry entry — every edge symbol-anchored and re-derived by a meta-lint that reddens on a broken anchor. Built from real drift: a fan-out over twelve models classified roughly six-hundred anchors and caught about fourteen genuine model↔code drifts — stale symbol cites, deleted-file registry keys, a prose cite the code had moved away from. The load-bearing result: for most of them no existing lint fired, so the graph was their first mechanical detection. That reprised the audit's near-one signal-to-noise and zero false positives on an independent, freshly-observed drift set — evidence that a mechanism designed from real drift catches real drift.
- The clean-versus-drifted split, on that same fan-out, re-confirming the governing principle: the models carrying a standing anchor-resolution lint drifted zero times; the drift concentrated in the registries with no such lint. Derived defended; snapshotted drifted.
- The two exemplars it generalizes: a per-model state-machine reconciliation lint whose symbol-presence references seeded the anchor type, and a coverage walk asserting every model element has a verified-by artifact.
- The active-implementation registry plus its pointer-agreement lint, seeded by a prod-blocking deploy incident where a built-but-unwired replacement left every pointer surface aimed at a deleted driver.
- Proof-as-anchor — the trajectory that folds formal methods into the graph. Where an invariant carries a model-check (a bounded-model-check or exhaustive state-space search, for the concurrency slice), the proof is just another anchor kind: a
verified-byedge whose target is a checker run rather than a test. Two payoffs follow. The agent's traversal reaches the whole verification story — invariant, the code it governs, the proof that clinches it. And when anchored code changes, the graph can trigger re-running the checker: for that slice, re-verification is mechanized, where every other edge's semantic-currency check stays sample-judged by hand.
Related Patterns
- Counterpart — drift & parity gates: a per-model model↔reality equality check. This generalizes that one edge kind into a typed graph spanning model↔lint↔code↔proof↔registry, and turns "does the edge still hold?" from a hand-maintained matrix into a re-derived walk.
- Enabler — executable source-of-truth: the typed models are the nodes this graph's edges terminate on; the graph is one more consumer of that substrate.
- See also — coverage → model-node mapping: a sibling join over the same nodes. That maps tests onto model nodes to show which invariants are exercised; this maps code, lints, and proofs onto them and re-checks that the joins resolve. Both make the model a work-list of unresolved joins.
- See also — control↔substrate dependency: the neighbouring self-application of the models to the fleet's own edges. That types each control's substrate assumption to compute a migration blast radius; this types each trace edge and re-derives it to catch a broken join. Both lift an invariant out of buried prose into a typed, queryable fact.
- See also — meta-model consumption: the read-don't-copy discipline the derived-over-snapshot invariant extends from a single value to a whole edge.
- See also — query surface: the read API a bidirectional trace query rides on, so an agent walks the graph up (code→model) or down (model→code) on demand.