English · 中文
Abstract what a design or a piece of code claims into a model and let an engine run it: findings carry citations and hashes, so they can be recomputed and compared. The conclusion comes from a run rather than from reasoning it out: thinking it through becomes running it. A native DeepSeek Harness plugin. It turns the assertions a design makes **about behaviour** into models that can be run, reviewed and exported: - **Check a claim**: against the source, cited to `file:line`. - **Run a model**: state machines, protocols, composed machines and data models become executable, and an engine runs them. - **Review a diagram**: read as a model, reviewed as a model, reconciled with it. - **Compare a refactor**: a model before and after, with the two reports side by side. - **Leave a record**: conclusions fixed into a report with hashes, recomputable and comparable and exportable. ## What it covers | Domain | What it does | |---|---| | Claim checking | Enumerates the verifiable claims in a design, spec or review comment. Checks each against the code with a citation, and says plainly which ones it could not settle | | Behaviour | State machines and protocols: structural checks, adversarial probes, budgets and deadlines, before/after regression. Composition checks catch deadlock and a rendezvous that never fires | | Diagrams | UML 2.5 diagram families: render, parse and modelling review (including the render→parse fidelity check), in Mermaid and PlantUML | | Structure | Component, package, class and deployment diagrams audited as dependency graphs: isolated nodes, dangling endpoints, cycles, matrix and layer violations, missing required edges | | Data | Data models and migrations: structure, migration coverage, copy consistency, rollback symmetry, before/after data regression | | Concurrency / synchrony / async | Mines claims about how work is executed (thread-safe, locks, interrupts, async/await, the event loop) and routes each to a tool that can decide it. It proves nothing itself | | Export | Exports a verified model as input for UPPAAL, TLA+, PRISM or SPIN | | Reports | Report body rendering, baseline comparison (`report_diff`), hash specification | ## Typical uses ### A refactoring harness A refactor may change the implementation. It may not change the behaviour. Let an engine settle that, instead of reading the diff: 1. **Before**: extract a BEFORE model from the code as it stands (`uml_parse` reads an existing diagram, or write the model against the schema). 2. **Refactor**. 3. **After**: extract an AFTER model. 4. **Regression**: `model_verify` with `beforeModel` and `stateMapping` runs the before/after regression: behaviour preserved, invariants continuous, the state mapping consistent. On the data side, `model_datamodel_verify` runs the same comparison over data, from its `beforeModel`, `fieldMapping` and `migrationMappings`. 5. **Verdict and record**: `report_diff` compares against the baseline report. An added error finding is the reason not to accept the refactor. The hashes in the report let the conclusion be recomputed. It compares the **two models you give it**, not two versions of the code. Whether each model is faithful to its own source is what steps 1 and 3 are for, and it does not do that part for you. It does not read the diff, edit code or run your tests either. It answers "is the behaviour still the same", not "was this a good refactor". ### Reviewing a code flow Draw the branching logic as a flow, then read what the picture actually says: 1. **Extract the flow**: write the branches of a function or a service as a `LogicModelV1`, or draw a `stateDiagram-v2` / PlantUML diagram by hand. 2. **Read it back**: give the hand-drawn diagram to `uml_parse`. A line it cannot read becomes a warning rather than disappearing. 3. **Review it**: `uml_review` reports the structural defects - unreachable states, dead ends, a branch that is ambiguous or not exhaustive, a self-loop with no exit, isolated nodes, cycles - and the documentation gaps. 4. **Reconcile with the source**: take every finding back to the code. A correct diagram does not make the code correct. It reviews the diagram and the model you give it. Whether they match the code is what step 1 is for. ### Reviewing a state machine Build the machine as an executable model and let an engine run it, instead of reading the code and concluding that it cannot get stuck: 1. **Build the model**: `uml_parse` reads a hand-drawn `stateDiagram-v2` or PlantUML state diagram; a `LogicModelV1` can also be written directly against the schema. 2. **Run the checks**: `model_verify` looks for unreachable states, absorbing cycles, events silently ignored, an allocation with no recovery path, a budget overrun, and a deadline that cannot be met. It reports each as a code whose prefix says which family it belongs to. 3. **State the always/never claims**: put them in `invariants`. The engine searches every reachable state for a counterexample and returns the shortest one it finds. 4. **Reconcile with the source**: every error finding goes back to the code. Concurrency claims split in two: the ones about **two models touching one shared location** are decided here, by `model_compose_verify` (declare `shared` and `accesses`; C3/C4/C5 decide the declaration, the unordered write and the lost update). Source-level data races, interrupt latency, a blocking call and a missing `await` are still routed to TSan/Helgrind/CBMC/TLA+. Hard real-time semantics - deadlines and periods - are outside its scope. ### Auditing a dependency diagram A component diagram is a claim about which modules may depend on which. Read it as a graph, then ask whether the edges are allowed: 1. **Give it the drawing**: PlantUML component, package, class or deployment source, or a Mermaid class diagram. `uml_structure_verify` parses it into nodes and edges. 2. **Say what is allowed**, if you have a rule: a matrix of `layers` and `rules`, each rule naming a `source` with `allow` / `deny` / `require` and a `default` for everything else. Without a matrix it reports only structural defects. 3. **Read the findings**: an isolated node, an endpoint never declared, a cycle with its shortest path, an edge that crosses a layer, a required edge that is missing, and - when no node is declared at all - that the input said nothing to audit. 4. **Ask the same question about a code flow**, if the drawing is a state or activity diagram: that is `uml_review`, not this. It audits the drawing, not the code. A drawing that is internally consistent can still be wrong about the system, so pair it with a source-side scan. When a hand-drawn diagram reports label drift, `uml_explain_labels` prints the label forms the parser accepts for that notation. ### Holding a design to its own declarations A design says things about itself: this layer sits above that one, this component owns that dependency, this interface is narrower than its callers. `model_design_review` decides whether the design keeps those promises: 1. **Write the design as a model**: the architecture (nodes and edges), plus what it declares - layers, boundaries, allowed and required edges, types with responsibilities, operations, transitions, supertypes. 2. **Run it**: `model_design_review` reports the places the design contradicts itself, and separately the shape of its graph - cycles and the fewest edges that break them, load-bearing elements, ranks, fan-in and fan-out. 3. **Read the three lists**: `violations` decide the verdict; `signals` are worth a look and fail nothing; `facts` is a measurement, not a finding. `checksSkipped` says which principles went unchecked because nothing was declared to hold the design to. It never judges a design by an outside standard. It reports that the design contradicted **something it declared**, or a structural fact about its graph. Asking whether the design is *good* is a question for a reviewer, and this tool answers a different one: does it hold together on its own terms. ### Two machines that have to agree One machine cannot deadlock *because of another one*. When two components hand-shake, the interesting failures live in the composition: 1. **Model each machine** on its own, then pass them together: `model_compose_verify` takes an array of models. 2. **Name the shared events** in `rendezvous` if a handshake is only legal when both sides are ready. An event not named there advances one machine, so a machine waiting on a handshake can take any number of its own steps first. 3. **Read C1 and C2**: a reachable node where no machine can advance and one of them is not terminal, and a rendezvous that can never fire. Both name the reason per machine, and C1 gives the shortest counterexample. There is no rate ratio and no fairness bound in the model. For one machine on its own - unreachable states, invariants, cost against budget - that is `model_verify`. ### Concurrency claims, mined and routed "Thread-safe", "lock-free", "ISR-safe" are claims that need a tool that can settle them, and the first job is finding them: 1. **Scan the text**: `model_interleaving_scan` takes the document, plan or notes and reports the risk points - the claim, the shared state, the interrupt, the critical section, and the async ones (`async`, `await`, `promise`, the event loop, a callback). Every finding carries a `family` (threads / synchronization / async / interrupts / shared-state), and an absolute claim is an error. 2. **Read what each absolute claim owes**: a claim like "no data race is possible" is reported as an error requiring dedicated verification, and each finding names the analysis that could settle it - TSan or Helgrind for a race, CBMC for a bounded proof, TLA+ for a protocol, RTOS-aware interrupt analysis for an ISR. 3. **Run that analysis**: this plugin does not run it and proves nothing about concurrency itself. It reads text. It does not see your threads, and a clean scan is not a clean bill of health - it means no claim was found, which is a different statement. ### A migration, before and after A migration is two models and a claim that the data survived. Give it both and the claim becomes checkable: 1. **Two models**: the schema as it was, and the schema as it will be, each a data model with entities, fields, keys and relationships. 2. **Say how fields move**: `fieldMapping` from the old path to the new one, plus `migrationMappings` for a field whose source is not simply its own old name. 3. **Run the comparison**: `model_datamodel_verify` with `beforeModel` checks migration coverage, copy consistency, rollback symmetry and the before/after data regression. 4. **Read the warning**: a field declared `required` in the new schema with nothing supplying it is reported as `DS2_REQUIRED_FIELD_UNSOURCED`. That is a warning, so the verdict stays `pass_with_findings` - it is a decision to make, not a failure the engine gets to declare. It compares the two models you give it. Whether either is faithful to the database it describes is the extraction step, and this tool does not do it. ### Importing and exporting diagrams: a frozen record, and a reference for the long run What is kept here is the **source file**, not a screenshot: `uml_render` writes Mermaid or PlantUML source, and `uml_parse` reads that source back into a model. One diagram therefore serves two purposes: - **A frozen record of the design**: commit the diagram source, the model and that round's verification report together, as the design as it stood at a point in time. The model may carry `_`-prefixed metadata - a ticket number, a date, an owner, the caveats left by the extraction - and those keys take no part in the hash, so archive notes do not change the identity of a conclusion. - **A reference for the long run**: on the next change, extract the model again, run the verification again, and compare with the frozen report through `report_diff`. An added error is what this change introduced; a finding that disappeared is an old problem solved. The hashes decide whether this is still the same model, instead of an eyeball comparison of two pictures. When an external checker is needed, the same model can be exported with `model_export` as native input for UPPAAL, TLA+, PRISM or SPIN. The limit: it stores and compares **model and diagram source**; a rendered picture is a by-product. A diagram that changed while the model did not - or the reverse - shows up at the next parse or comparison. ## Tools | Tool | What it does | |---|---| | `uml_render` | Model → diagram source (Mermaid or PlantUML) for a chosen family. A view the notation cannot express is refused, with the reason | | `uml_parse` | Diagram source → the family model. A text that is not a state machine or flow is refused by name, not read as one | | `uml_review` | Audits the modelling: structural defects, documentation gaps and render↔parse fidelity. Give it a model, a diagram, or both | | `uml_explain_labels` | Prints the label and comment contract the parser accepts; no diagram needed | | `model_verify` | Executable verification of state machines and protocols | | `model_compose_verify` | Two or more machines together: deadlock, a rendezvous that never fires, and - with `shared` and `accesses` declared - an unordered write (C4) or a non-atomic read-modify-write pair (C5) | | `model_datamodel_verify` | Data models and migrations | | `model_interleaving_scan` | Mines and routes concurrency, synchrony and async claims | | `model_export` | Exports to an external checker (UPPAAL, TLA+, PRISM, SPIN) | | `uml_structure_verify` | Dependency-graph audit, including a dependency matrix and multi-level refinement | | `model_design_review` | Design review: the dependency graph's shape, plus the contracts the design declares about itself - layering, responsibility boundaries, substitutability, interface width | | `report_diff` | Compares two reports: what a change added, removed or changed | ## Reading a report What a tool returns is a report, and the outcome is in `verdict`: read `verdict`, never `ok`. `ok` carries a different historical meaning in each family — most set it to `true` for a failing review, and a composition sets it to `false` when any error-severity finding exists — so it cannot be read as a verdict, and reading it as one is how a reader concludes the opposite of what the report says. | Field | Meaning | |---|---| | `verdict` | The outcome: `pass`, `pass_with_findings` or `fail` | | `verdictReason` | One sentence saying why the verdict is what it is | | `hashes` | `hashSpec` and `modelHash`; a regression also carries `beforeModelHash` and `afterModelHash`. The same model always hashes to the same value | | `nextSteps` | What the engine suggests doing next | | `schema` | The versioned report contract, for example `model-everything/verify/v1`. Branch on this field rather than on the shape of the payload | | `truncated` | The search hit its ceiling and stopped. **A truncated search is not a pass**, it is no conclusion; a property that could not be decided appears as `_UNDECIDED` | The body is what comes back by default. For the whole structured result, pass `reportView: "full"`. When `ok` is `false` the verdict is `fail` as well, but it means something else: the tool did not run. The reason is in `errorCode` - invalid input, an unsupported diagram family, or a declared `intent` this view cannot serve. Such a refusal starts its `verdictReason` with `the tool did not run:`. The method behind reading one of these has a home of its own: [`skills/model-everything-report-reading/`](skills/model-everything-report-reading/) gives the reading order (did it run, what did it decide, what next), where each family keeps its findings, and the two readings that are easy to get backwards. Its structure comes from a **generated mind map**: [`docs/report-reading/mindmap.mmd`](docs/report-reading/mindmap.mmd), and `tests/report-reading` fails when the map and the engines disagree. `uml_render`, `uml_parse` and `uml_review` take one more field, `intent`, which says what the artifact is for: a human will read it (`present`), the verification engine has to read it back (`verify`), or the point is to prove the render matches the model (`fidelity`). A view that cannot serve the declared purpose is refused rather than drawn anyway. ## Examples `examples/` holds sample models that run as they are, with [`examples/README.md`](examples/README.md) saying what each one shows and what to expect. They are documentation, not test fixtures — every suite reads its own `tests/