TECHNICAL WHITE PAPER

Mermaid Diagram Driven Development: Idea Limbs for Agentic Software Engineering

Abbreviation: MDD Original date: May 2026 Last revised: August 2026 Document revision: 0.2.5 Classification: Open Technical Standard Proposal Target Audience: AI Systems Architects, Agent Runtime Teams, Formal Methods Engineers, Software Engineering Researchers

Abstract

Current LLM-based software engineering workflows treat knowledge as passive reading material: Markdown, vector stores, long-context prompts, retrieved snippets. Agents reinterpret those artifacts on every task, and nothing tells them when an artifact stopped matching the source it was written from.

Mermaid Diagram Driven Development (MDD) turns knowledge into an idea limb: a source-grounded, typed, reviewed, bundled design space that an agent traverses as an active capability instead of reading as prose. Mermaid is the first auditable graph abstraction above source material; typed MDD-IR is the canonical substrate beneath it, carrying source links, review findings, backend obligations, approval evidence, and the deterministic transition table a runtime enforces.

The limb is not the whole software system. It is a constrained operational surface derived from source material, checked at explicit gates, and packaged for deterministic runtime use. MDD validates a design-level abstraction and records the concrete backend evidence that actually ran. It does not claim to prove an implementation correct.

This paper describes the model and the v0.2.5 reference implementation at the level of what is true, not at the level of command lines. Exact invocations, flags, and artifact shapes live in each CLI's --help and in the operating guide that mdd-agent init scaffolds into a repository at .mdd/AGENTS.md; they are not restated here beyond a single golden-path example.

1. Core Thesis

An idea limb is knowledge converted from passive reading material into an active, source-grounded, typed, reviewable, and runtime-constrained capability for an AI agent.

A document tells an agent what someone believed. A limb tells an agent what it is currently allowed to do, and refuses to answer when the ground it stands on has moved.

Three properties separate the two:

It is bound to bytes. Every node and edge can carry a link to a source file, a selector into that file, and a content hash of the exact excerpt the claim was made against. When the bytes change, the binding breaks and the gate fails closed rather than degrading quietly.

Its authority is derived, not asserted. The status of a graph is computed on demand from evidence artifacts — compiler output, deterministic backend runs, an accountable approver's recorded identity and basis over reviewed evidence (a record, not a cryptographic signature). No rung can be reached by editing a label in a JSON file.

It is enforced at traversal time. The agent proposes an intent; the runtime decides whether the transition is legal, using the compiled bundle as the authority. Rejection is a first-class answer that carries its reason.

Mermaid diagrams are the auditable map of that limb. LLMs supply semantic interpretation against linked evidence and are never the source of authority. Deterministic tools validate hashes, selectors, typed graph structure, and traversal constraints; explicitly requested formal backends add scoped bounded-path or state-integrity evidence on top.

2. System Architecture

One pipeline runs from source material to agent traversal:

source docs / code / tests / logs / policies
  → mdd-agent idea init          idea capsule, obligations DAG, draft source map
  → Mermaid audit graph          the human-reviewable abstraction
  → mdd-engine compile           typed MDD-IR
  → source-link / source-check   hashes, selectors, excerpt drift — fail closed
  → review-source-map            per-target semantic findings (evidence, not proof)
  → verify                       scoped TLA+ / Z3 / Lean4 obligations, when explicitly requested
  → approve-edge                 per-edge Gold, bound to reviewed evidence and live bytes
  → bundle + attest              evidence-carrying, hash-chained .mddbundle
  → mdd                          deterministic traversal for downstream agents

The combined mermaid-engine distribution ships three entrypoints over that pipeline. mdd-agent formulates and grows the idea limb and orchestrates the LLM-dependent lanes; mdd-engine is the heavy compiler and deterministic checker; mdd is the lightweight, solver-free traversal runtime.

The compiler/runtime split is essential. Full verification may require LLMs, Java and TLA+, Z3, Lean4, and expensive model-checking runs. The standard distribution installs none of those external tools and no solver — concrete Z3 queries require the optional mermaid-engine[z3] extra. The mdd runtime travels inside the same distribution rather than as an independently packaged artifact, so refinement and backend checks happen once on the producer side and downstream agents consume the emitted portable .mddbundle, enforce its compiled traversal rules, and read its recorded verification status without rerunning any of it.

Every subcommand of all three CLIs speaks one machine contract: exactly one JSON object on stdout, exit 0 for ok: true, exit 1 for a semantic no, exit 2 for a malformed invocation, and stderr that is never machine-parseable; only --help and --version print human text. Replay files pin every live LLM gate to recorded output, so a run can be reproduced without a model in the loop.

The golden path needs none of the optional machinery — no formal backend, no LLM review, no approval, no trust anchor, because a draft bundle carries no trust claim and is freely inspectable:

mdd-engine compile diagram.mmd --out diagram.ir.json
mdd-engine source-link diagram.ir.json --mapping source-map.json --out diagram.sourced.ir.json
mdd-engine source-check diagram.sourced.ir.json --out source-check.json --require-edge-coverage
mdd-engine bundle diagram.sourced.ir.json --out diagram.mddbundle --source-check source-check.json
mdd view diagram.mddbundle

The idea limb workspace

mdd-agent idea captures an idea as a capsule — claims, assumptions, a draft source map, and a typed obligations DAG — then grows it from feedback or from an analysis report. Nothing in the workspace is stored twice: status, frontier, and next agent actions are derived at read time from the obligations DAG on disk, the attached diagrams whose IR still loads, and the outstanding debt. A workspace cannot report progress it does not have.

The workspace tracks three kinds of debt. Proof debt is obligations not yet discharged. Growth debt is proposals recorded but not yet folded in. Temporal debt is edges left untyped in a hand-edited IR, plus temporal edges whose causal likelihood is still possible or speculative; it is a status-report field, not a node in the DAG. Freshly compiled edges default to the transition type, so a new diagram reporting zero temporal debt is not a clean bill of health — debt appears once edges are deliberately typed.

mdd-agent write answers questions from the limb under an explicit authority precedence: human-approved Gold edges outrank agent-approved Gold, which outranks draft graph items, which outrank the model's own inference. Generated prose must end in a machine-readable claims block citing stable node and edge IDs; claims are then reconciled deterministically against the graph, the weakest cited authority wins, unknown IDs are flagged rather than accepted, and an adversarial judge pass attempts to refute each claim. Model output never mutates the IR.

Autoform-inspired source-to-target lifecycle

MDD adapts the useful shape of prior art — source corpus, declared targets, dependency DAG, deterministic gates, evaluation, trace learning — into MDD-native artifacts. Autoform Bot is non-commercial prior art only; Mermaid Engine vendors none of its code, prompts, docs, or test data, and the product boundary stays at deterministic CLI artifacts with replay files for LLM-dependent steps.

The obligations DAG is the work list: typed items for source review, formal backends, bundling, runtime smoke, and Gold approval, advanced through their statuses under enforced dependencies. Completing an item whose prerequisites are unmet is refused unless the out-of-order completion is explicitly forced and recorded as such, and deleting an item that others still depend on is refused the same way. eval-run reconciles a run directory's artifacts and fails closed on missing IR, source-map gaps, stale source checks, unsupported or incomplete review findings, verification overclaims, bundle manifest gaps, or Gold claims without approval evidence. learn failure turns failed traces into advisory guides — guides that may help a future run but can never override a parser, source, verification, backend, or Gold guardrail.

3. Mermaid as an Auditable Abstraction

Mermaid is valuable because it is compact, readable, diffable, and LLM-friendly. It gives humans a reviewable surface between prose and formal models. It also proves nothing: valid Mermaid syntax is not semantic correctness.

The reference compiler therefore accepts a strict subset and fails closed outside it. A flowchart or graph header carrying a direction must precede any body line; NodeId[Label] declares a node; Source -- event --> Target, Source --|event|> Target, and Source --> Target declare edges. Every line must match a supported form in full — arrows are exactly -->, trailing text after an otherwise valid form is rejected, and an inline bracket label binds the source node only, so labels belong on standalone declaration lines. Anything else produces a line-numbered diagnostic instead of silently dropping semantics; exploratory work can opt into lossy parsing, which records lossy_parse and the diagnostics in the IR rather than hiding them.

Two forms bite in practice. The most common Mermaid labelling syntax anywhere else, Draft -->|all edges approved| Gold, is not accepted — normalize it to Draft -- all_edges_approved --> Gold, because edge labels in MDD are deterministic transition identifiers rather than prose captions. stateDiagram is not supported at all.

Every graph element carries a provenance record naming the source file and line it came from; the v0.2.5 implementation records parser-derived elements as source_backed. A richer epistemic vocabulary — distinguishing explicit support, inference, model hypothesis, and human confirmation — is roadmap vocabulary, not shipped semantics. A diagram is a claim about a larger source reality, and provenance is where that claim states where it came from.

4. Source Grounding and Drift

Provenance labels are assertions. Source grounding is what makes them checkable.

A source map records the source artifacts a diagram is derived from — stable ID, kind, path, and content hash — and the links binding graph targets to locations inside them. Each link names its target, its source, a selector, and the claim the source is said to support.

Selectors come in two forms, and the difference matters more than it looks. A line span is exact and brittle: an edit above it slides every claim below, the link still resolves, and re-linking silently accepts the wrong location. A symbol selector names a Python definition by qualified name and re-resolves through the stdlib AST against the live file (Python sources only in v0.2.5), yielding the definition's current span including decorators. Nested and dotted paths are addressable; failures are actionable, naming near-miss candidates or reporting genuine ambiguity rather than guessing.

Both selector types record an excerpt content hash at link time. That single field is what converts grounding from a pointer into a binding, and it lets the deterministic source check report three distinct verdicts per link instead of one:

• Selector error — the selector no longer resolves at all. Fails.
• Drift — the selector resolves but the excerpt's content changed, so the claim was reviewed against different text. Fails, with a narrower diagnosis than whole-file staleness. Because a line span simply reselects whatever now occupies those lines, moved content reads as drift for line spans; only symbol selectors can tell the two apart.
• Relocation — a symbol selector re-resolved to new lines whose normalized excerpt content (trailing whitespace stripped per line) is unchanged. Informational, does not fail. This is the entire payoff of symbol selectors.

Whole-file staleness still fails on its own. Drift reporting refines the diagnosis; it never weakens the fail-closed gate. Coverage can additionally be required, failing when any node or edge lacks a source link.

Semantic review as evidence

Deterministic checks establish that a claim still points at the text it was made against. Whether the text actually supports the claim is a semantic question, and MDD answers it with an LLM under strict framing: the output is evidence, never proof. Live source review is also an explicit disclosure boundary: every allowed root is opened and descriptor-pinned before any source, then every source-path component is opened relative to that retained root descriptor with no-follow semantics. The declared root pathname must continue to identify the same directory throughout each read. Selector resolution and prompting use one immutable exact-byte snapshot that must match the IR source hash. Transient or persistent root replacements, source-path swaps, symlink escapes, and stale hashes fail closed before disclosure; every live provider requires explicit consent, while replay files do not.

Review runs per target — one call per (target_type, target_id) pair owning all of that target's links, so sibling links are judged together as complementary evidence for one claim. This is not a packaging detail. A single whole-map call put every target's evidence into every other target's context; measured on an identical IR, that design flipped more than half its verdicts between runs, and it rewarded authors for writing one giant span per edge, which is worse grounding. Smaller prompts are the reproducibility lever.

Each verdict is supported, contradicted, missing, oversimplified, or ambiguous. A verdict cache keys each finding by a hash over everything the verdict depends on — the same binding material approval uses, the exact rendered prompt, the provider, and the model — so re-reviewing after a one-edge change costs one call rather than one per target, and switching model or provider necessarily invalidates the entry rather than silently reusing another reviewer's judgment. The cache is a locally trusted input, exactly like source code on the same machine: its structure is validated on load, every reused verdict records its provenance, and one from an untrusted origin must never be adopted. A target whose response cannot be parsed is recorded as a failed target rather than discarding the run, and a failed target counts as unreviewed everywhere downstream.

5. MDD-IR and Edge Semantics

MDD-IR is the canonical typed representation, separating Mermaid syntax from formal semantics. It carries source artifacts, hashes, selectors and their excerpt hashes; graph kind; stable node and edge IDs with labels, provenance, actors, and events; guards, preconditions, and postconditions; finite semantic domains; environment actions; safety invariants, liveness candidates, and fairness assumptions; forbidden transitions; coverage obligations; backend projection hints; per-edge approval status with review-binding snapshots (the review findings themselves live in the separate source-review artifact); and edge relation types with temporal axes.

Finite semantic domains deserve emphasis. Vague prose such as "handle auth edge cases" is not checkable. Enumerating the domain — a refresh token is valid, expired, revoked, replayed, or malformed — turns it into enumerable states the design can be checked against. Today's backends check bounded transition projections of that structure; full domain and guard evaluation remains roadmap work (§7, §13).

Relation types and temporal axes

Every compiled edge carries one relation category: transition, dependency, semantic, or temporal. The category is additive and derived when absent, so every existing IR stays valid and every existing diagram compiles unchanged.

Temporal edges carry three orthogonal axes plus a rationale: ordering (precedes, concurrent, unordered), causality (causes, enables, prevents, requires, or none), likelihood (bucketed, never numeric), and a human-language basis for the mechanism. Ordering is the weakest claim; a non-null causal value is a mechanism claim and should be backed by its basis. One shared ontology is the point: the same categories and axes mean the same thing in the compiler, in the analysis lanes, in the bundle, and at runtime, and a compact deterministic string form lets external systems store the typing without inventing a parallel vocabulary.

The contract is signals, not gates, with the line drawn at well-formedness. Schema validation of the category and axes may hard-fail with diagnostics — malformed data is not a semantic disagreement. Semantic interpretation of well-formed temporal edges only de-prioritizes: analysis emits weighted advisory signals, never removes an edge, never fails verification, and never changes binary status.

Typing enters through an IR-level operation, never through Mermaid syntax — Mermaid remains a view. Typings apply atomically, validated in full before anything is written, preserving every unrelated field and provenance record. Typing a Draft edge does not promote it; changing the semantics of a Gold edge invalidates its source-review binding, removes the approval, and returns the edge below Gold until current evidence is reviewed and approved again. Typing is a proposal; approval remains the gate.

Approved impossibility

There is one place where a soft temporal claim becomes a hard gate. When an edge typed as preventing its target receives Gold approval against current evidence, it is promoted into the IR's forbidden set. From then on every verification backend drops it from the checked transition relation — so the backends all agree on one model — and every runtime surface refuses it with an explicit forbidden reason, reporting it separately from legal transitions.

Impossible transitions therefore stay visible to agents and are never traversable. "Impossible" is an approver's promotion of a soft signal (a user, or an explicitly supervising AI agent), not an inference the tooling makes on its own, and the invariant holds in both directions: retyping a Gold prevention edge retracts the forbidden record along with the approval, and re-approving the new semantics promotes it again.

This closes the idea loop. Hypothesize a relation by typing an edge, collect formal and analytical feedback, then approve it or retract it. Until that resolves, a speculative temporal claim stays visible in the idea workspace as temporal debt.

6. The Derived Metal Ladder

Status is derived from evidence artifacts, never stored or promoted. Each rung is minted by a different class of validator — the compiler, deterministic backends, and finally an accountable approver — so no rung can be reached by editing a label:

• Draft — a generated or compiled candidate graph; source grounding may be unknown.
• Source-linked Draft — a descriptive stage (not an emitted rung: the computed profile reports draft, bronze, silver, or gold) where source artifacts are bound by stable IDs, hashes, and selectors.
• Bronze — a valid, source-linked IR with at least one backend proposal bound to the current IR.
• Silver — Bronze plus a current source-check pass and verified backend execution bound to the current IR hash; authority-bearing records are independently re-executed against the exact IR, and the locally selected tool identity, obligation inputs, outcome, witness, and model-check counts must match the record. Where a semantic-introspection artifact (the deep-review lane's backend-recommendation step) is supplied, every recommended backend must be verified.
• Gold edge — a user or explicitly supervising AI agent approved that edge on top of a Silver profile, using current supported review evidence, with the binding matching the embedded snapshot and engine-side validation confirming the producer source bytes are still current.
• Gold diagram — the rollup where every edge is a currently valid Gold edge.

Because the middle rungs are computed from evidence, they demote automatically: edit the graph and the bound verification manifest stops matching the IR hash; let a source drift and the rerun source check fails — either way the profile recomputes lower. Semantic reviews remain mandatory gates in the deep-review lane and feed approval evidence, but they no longer mint status — only deterministic backends and accountable approvers do.

Gold is deliberately per edge. A diagram can be Silver with some Gold edges while remaining non-Gold overall. Approving one edge requires that edge's own findings to be supported, that edge to have been reviewed rather than missing or failed, its findings to cite only current links, their union to cover all of that edge's current links and match its current sources, its binding to match the live IR and source bytes, and every current link to carry an excerpt hash. Several supported findings for one edge are credited together, so decomposed per-link verdicts add up. A contradicted verdict on one edge blocks that edge and nothing else — with review flakiness measured in double digits on identical inputs, a global gate made Gold honestly unreachable.

Approval binds the reviewed edge semantics, links, selectors, claims, source records, and current producer source bytes. Engine-side validation, verification, and bundling reread those bytes and fail closed on staleness. If a source has moved, it must be refreshed, remapped, re-reviewed, and re-approved; if introspection expands a Silver or Gold diagram with new edges, those edges inherit nothing and the diagram re-enters review.

Semantic compression and refinement

A top-level diagram should express the solid idea, not every hidden dynamic. A coarse parent edge may stay compressed and still be approved at the abstract level. When detail matters, MDD attaches a refinement subdiagram instead of flattening internal states into the parent:

Parent diagram:  A -- important_transition --> B
Subdiagram:      A -- micro_step_1 --> X -- micro_step_2 --> B
Projection:      A .. X .. B collapses back to important_transition

Refinement is a contract, not decoration — and in v0.2.5 it is a specified contract, not a shipped workflow (the roadmap lists it as Partial). The IR carries refinement link targets, and the intended lifecycle is modeled in TLA+ in this repository (specs/DiagramEvolution.tla with specs/DiagramEvolution.cfg), checking that approval evidence is properly chained, that Gold cannot appear without current source and current supported review, and that staleness or expansion returns a diagram to Draft until it is remapped and re-reviewed. The intended semantics: an attached subdiagram must preserve the parent edge's entry and exit meaning, classify every terminal path, and pass projection checks; parent Gold never transfers downward. No CLI yet attaches or checks subdiagrams.

7. Scoped, Honest Verification

MDD uses three formal backends, each for a specific and deliberately narrow job. What matters more than their coverage is that the tooling never reports evidence a backend did not produce.

TLA+ is the state-space integrity layer. Given a model checker and the explicit check flags, the engine emits a finite module and configuration from the compiled IR and checks well-typedness plus deadlock freedom over the emitted transition relation, with exact node and edge coverage recorded in the generated module. It does not yet encode rich guards, domains, liveness, fairness, refinement, or temporal requirements beyond that transition model.

Z3 handles bounded reachability over the finite transition relation, when a start, target, bound, and expectation are explicitly requested and the optional mermaid-engine[z3] extra is installed. A concrete query records solver version, bound, expectation, the reachability booleans, and a witness path when one exists. It is not full guard evaluation, and it is not a liveness or fairness proof.

Lean4 checks generated finite transition obligations — state and edge definitions plus one source/target soundness theorem per edge — when Lean and the explicit check flags are supplied. It does not yet prove rich semantic extrapolations, runtime guard semantics, refinement, or fairness. Lean is not a semantic oracle: it checks formalized definitions, which an LLM may propose but deterministic tooling must check.

Proposal-only versus concrete

The single most important honesty property in the command surface is that selecting a backend is not running one. The selection flags are proposal-only acknowledgements; execution requires the corresponding concrete check or query flags. Plain verification is IR validation and says so in its manifest. A separate proposal command emits LLM-authored candidate backend artifacts, and its name is its contract: verification never executes them, and their existence is never evidence. A command that reported success after doing no solving would be a correctness trap for an audience of agents, so proposal and proof are separated at the command surface rather than in a footnote.

A bundle is marked verified only when its manifest contains structurally complete, internally consistent, successful concrete backend evidence. Before such evidence can mint Silver, Gold, or verified: true, the engine re-executes each recorded obligation using locally selected tools rather than record-supplied commands or paths and compares the authority-bearing result fields. Z3 authority requires a non-vacuous obligation with distinct start and target states and a positive bound. Only mdd-source-review-approval/v1 can carry Gold authority: legacy-v0 approval bindings contain no formal replay binding or receipt, so engine validation, bundling, and portable runtime loading reject them; historical records require fresh v1 approval before Gold use. Gold approval retains an engine-generated replay receipt and a hashed canonical pre-approval formal-model projection containing only the topology and temporal fields consumed by the concrete backends. Bundle production re-executes every distinct Gold receipt against its own retained projection and carries the deterministic result set as approval_authority; each edge is matched to the replay identified by the SHA-256 of its exact verification binding, so approvals from different lifecycle snapshots remain valid without sharing authority. Changing and self-rehashing a projection does not help if real backend output no longer matches. If the caller separately supplies verified evidence for the final approved IR, bundling also re-executes that evidence against the exact final IR and retains it as authority with mode local_execution_replay. Caller-authored backend JSON is never retained as either authority object. This two-phase model matters because Gold approval of a temporal prevents edge intentionally changes the final transition relation after the Silver check.

Hard gates and soft signals

Verification is the hard gate and the CI entrypoint, so what CI enforces is exactly what a developer reproduces locally. Analysis is the soft lane: it never gates, never exits nonzero for a semantic finding, and never changes binary status. It writes weighted advisory signals, each attributed to the tool that produced it, the graph item it concerns, and the receipts behind it, so a consumer can always tell an observation from a verdict.

The route lane is deliberately solver-free and says so in its own output. It is deterministic best-first route enumeration over the transition relation: expansion prioritizes lower-penalty frontier entries, but route and expansion caps make a truncated run incomplete and possibly omit routes, so every report states whether the bounded space was exhausted and records its expansion count. Signals are aggregated per edge, never per route, so one assertion is never multiply counted. An unapproved prevention claim stays advisory but dominates accumulated uncertainty by construction; once approved into the forbidden set, its edge leaves route expansion entirely and is reported separately. The ordering lane projects ordering and prevention onto the finite model and reports tensions, labeled as read off the IR's typed axes rather than produced by model checking. Given a model checker, analysis may run a second, non-gating model whose violations surface as genuine counterexample signals — separate from, and leaving untouched, the gating invocation.

CI must compose the gates it intends to enforce: compilation owns supported Mermaid parsing, plain verification owns IR validation, source checking owns hash, selector, target, and coverage integrity, approval owns the current-supported-review precondition for Gold, and explicit backend flags own only the obligations they execute. Attributing all of that to one command is the mistake the surface is shaped to prevent.

8. The Trust Boundary

An evidence-carrying bundle travels. Where it lands, the producer's files do not exist. Everything about MDD's trust model follows from that asymmetry.

A bundle carries its metadata and hashes, the canonical IR with its source map and approvals, a deterministic transition table, a verification manifest, and optional semantic-index, source-check, source-review, and advisory analysis artifacts. Attestation records a hash chain over it: the attestation covers the manifest, and the manifest's hashes cover every bundled file, so validation checks the whole chain and tampering with any inner artifact fails. This is a deterministic integrity chain, not cryptographic signing — no key, no signer identity, no non-repudiation. An attacker who can rewrite the bundle can rewrite the attestation beside it. Real signing remains roadmap work.

The consequence is precise and unavoidable: a self-rehashed bundle cannot authenticate itself. Consuming any Gold edge, or any bundle whose manifest claims verification, therefore requires an externally trusted SHA-256 of the bundle manifest, supplied by flag or environment variable. Without it, loading fails closed. That digest must arrive through a trusted producer or release channel; recomputing it from the received bundle proves exactly nothing.

Given the anchor, portable loading validates the embedded rollup and approval bindings without needing producer source paths. What it establishes is bounded, and stating the bound precisely matters: the runtime authenticates producer-bound assertions. It confirms that a symbol link is structurally well-formed, carries its frozen resolved span and excerpt hash, and is the assertion the anchored producer bound. It does not re-resolve the selector or re-read the excerpt — with no producer files on the machine, that is impossible — so it never establishes that the symbol still exists or still says what the claim says. Recorded drift is treated as blocking. The producer side, which does have the files, is where live bytes are reread and staleness fails closed.

9. The Runtime as Action Policy

mdd is not a verifier. It is the action policy an agent runs under: it loads a bundle, validates its hashes and — given an attestation — the full integrity chain, exposes states, nodes, edges, and legal operations, checks proposed transitions, rejects illegal ones with reasons, enumerates and ranks bounded routes without a solver, resolves approved fuzzy utterances through a bundled semantic index, validates agent-supplied traces, and returns machine-readable JSON throughout.

The protocol is four lines: the LLM proposes an intent; the runtime computes the legal transitions; the LLM chooses among them and appends the step to its trace file; the runtime validates the whole trace (mdd trace) and rejects any illegal step. If a transition is rejected, an agent must not route around it — it inspects the alternatives, explains the rejection, repairs the graph through the engine, or asks for human review. One unified view command is the preferred entrypoint when an agent wants current state, available operations, verification level, approval status, and approved aliases in a single object.

Route ranking is pure graph search: bounded routes carry a per-step attribution recording which edge contributed which weight, under which likelihood, and the rationale behind it, so an agent can see why one timeline ranks above another instead of trusting a single number. Immediate-edge ranking is a deterministic sort sharing the same penalty model and default bound, so weights are comparable across the two. Because enumeration is capped, results always state whether the whole traversable bounded space was seen. Advisory analysis can live inside the bundle, so ranking needs nothing beyond the bundle itself; bundles without edge types load and traverse identically, because typing alone does not alter legality while approval into the forbidden set does.

Semantic fuzziness is deterministic and fail-closed. A semantic index accepts only approved mappings citing human approval or a named, versioned external policy such as a translation, glossary, or controlled vocabulary. Resolution checks exact legal edges first, then selects only among currently legal outgoing transitions; ambiguity returns candidates instead of choosing arbitrarily. The runtime never invents a transition.

10. Design-Debugging Principles

The AWS paper "Use of Formal Methods at Amazon Web Services" (Newcombe et al., CACM 2015, https://cacm.acm.org/research/how-amazon-web-services-uses-formal-methods/) teaches that formal methods succeed in industry when framed as debugging designs. AWS found prose, diagrams, reviews, tests, and fault injection necessary but insufficient: subtle bugs lived in the design itself and surfaced only under rare interleavings of failures, retries, crashes, recoveries, reorderings, and operator actions.

MDD adopts four consequences of that lesson.

Start from what must go right. Before drawing the happy path, enumerate safety invariants, liveness candidates, forbidden transitions, recovery obligations, environment assumptions, and the source provenance of each — then draw.

Model the environment with the system. A model containing only the application's happy path is misleading. For agentic software the environment is first-class and includes timeouts, message loss, duplication and reordering, crashes and restarts, external service errors, operator actions, user corrections, permission denials, tool failures, malformed tool output, stale memory, conflicting instructions, invalid LLM intents, and the retry, backoff, and recovery behavior that responds to them.

Prefer small bounded dangerous models. AWS found serious bugs in small models. Build the smallest finite model that can expose the dangerous behavior, omit implementation detail that no stated property depends on, and state every abstraction decision.

Know the scope. MDD is strongest for state and path validity, forbidden transitions, workflow and recovery correctness, agent traversal constraints, interleaving risk, semantic edge-case coverage, and source-backed design documentation. It is weak, unless separately modeled, on emergent performance collapse, queueing and load dynamics, hard real-time latency, probabilistic availability, adversarial economics, and implementation correctness without tests, assertions, and instrumentation.

11. Related Work and Differentiation

Spec-driven AI development — GitHub Spec Kit, OpenSpec, Kiro Specs, spec-workflow-mcp — validates the demand for structured AI-native development, but organizes requirements, designs, and tasks as Markdown and workflow rather than compiling them. Spec tools organize intent; MDD compiles intent into state and path constraints and records scoped check evidence.

Agent graph runtimes — LangGraph, XState, Stately Agent — show the value of graph and state-machine control for agents. Graph runtimes execute workflows; MDD source-checks the semantic graph, records explicit backend evidence, and constrains traversal against it.

Formal methods — TLA+, Apalache, P, FizzBee, Alloy, Lean4 — provide the verification backbone, and AWS's industrial use demonstrates that design models find bugs conventional methods miss. Formal tools require formal authoring; MDD provides the source-document to Mermaid to typed IR to backend to runtime-bundle pipeline that gets a team there.

LLMs for formalization — assisted specification, proof generation, proof-carrying completions — shows models can help produce formal artifacts. That work usually targets specs and proofs directly; MDD inserts an auditable graph layer in between and emits runtime traversal constraints.

GraphRAG and knowledge graphs extract document graphs for retrieval and synthesis. GraphRAG answers questions from document graphs; MDD compiles state and path semantics out of them into checkable, traversable artifacts.

12. Contribution Claims

1. Source-provenanced Mermaid abstraction: a human-auditable layer between natural language and formal models, with fail-closed parsing.
2. Binding rather than pointing: symbol selectors that survive edits, excerpt content hashes that make grounding a binding, and a check that separates relocation from drift from staleness.
3. Typed MDD-IR: a canonical graph with stable IDs, provenance, per-edge approvals, relation and temporal metadata, and backend projection fields.
4. Derived status: a metal ladder computed on demand from evidence bound to the IR hash, which demotes automatically and cannot be reached by editing a label.
5. Scoped multi-backend verification: explicit, narrow TLA+, Z3, and Lean4 obligations, with proposal and proof separated at the command surface.
6. Evidence-carrying bundles under an explicit trust boundary: checks, reviews, backend status, and transition tables travel together, and portable consumption of Gold or verified claims requires an external trust anchor.
7. Agent traversal protocol: LLMs propose intent; deterministic runtime logic disposes, with rejection as a first-class answer.
8. Environment-aware modeling discipline: failures, retries, tool errors, user corrections, operator actions, and invalid LLM intents are modeled with the system.

Unlike spec-driven tools, MDD does not stop at structured Markdown. Unlike graph runtimes, it does not merely execute workflows. Unlike formal methods tools, it does not require engineers to author raw formal specifications. MDD introduces a source-provenanced Mermaid layer and typed graph IR that compile into scoped formal backends and lightweight runtime bundles for AI agents.

13. Limitations

• A model with concrete verification evidence is still not the real system.
• Source documents may be incomplete, stale, contradictory, or simply wrong; grounding binds a claim to text, not text to truth.
• Semantic review finds unsupported abstractions, but LLM review evidence is not deterministic proof, and it is not perfectly reproducible.
• LLM extraction may mislabel semantics.
• Formal checks cover only encoded assumptions and bounded domains; Lean checks formalized definitions, not informal intent.
• The runtime checks proposed transitions against the compiled bundle, not against global reality, and authenticates producer-bound assertions without being able to re-resolve them.
• Attestation is tamper detection, not signing; there is no signer identity and no non-repudiation.
• Implementation correctness still needs code review, tests, assertions, monitoring, and integration discipline.
• Performance collapse, queueing dynamics, probabilistic availability, and adversarial economics must be explicitly modeled or marked out of scope.

The mature claim is that MDD verifies scoped design-level state and path obligations when concrete backends run, and constrains agent traversal under the bundle's declared assumptions. Not that MDD proves the software correct.

14. Implementation Roadmap

15. Conclusion

MDD converts raw knowledge into idea limbs: source-grounded workspaces, auditable graphs, typed IR, explicit obligations, honest verification manifests, portable bundles, and logic-guided agent behavior. mdd-agent formulates and grows the limb, mdd-engine compiles and checks it, and mdd lets agents traverse it without inventing invalid paths.

Mermaid-based, source-provenanced, bounded and explicitly checkable idea-limb construction for AI-assisted software engineering.

The goal is not prettier diagrams. It is to convert passive knowledge into an active, bounded capability that agents can inspect, grow, verify, bundle, and traverse — without hiding uncertainty or overclaiming proof.