Verification Guide
A hands-on walkthrough of the three verification layers in GDS, using deliberately broken models to demonstrate what each check catches and how to fix it.
Three Verification Layers
| Layer |
Checks |
Operates on |
Catches |
| Generic |
G-001..G-006 |
SystemIR |
Structural topology errors |
| Semantic |
SC-001..SC-007 |
GDSSpec |
Domain property violations |
| Domain |
SF-001..SF-005 |
DSL model |
DSL-specific errors |
Each layer operates on a different representation, and the layers are complementary: a model can pass all generic checks but fail semantic checks (and vice versa).
What Verification Does Not Cover
All three layers check structural consistency — does the model obey the rules of its own declared categories? They do not check whether those categories were chosen well. A stock-flow model where "customer satisfaction" is declared as a Stock will pass every check — whether satisfaction actually accumulates like a stock is a judgment call that no formal check can answer.
This is the boundary between verification (automated, structural) and validation (human, domain-specific). Verification asks: "Given the roles and state variables you declared, is the model internally consistent?" Validation asks: "Did you declare the right roles and state variables for this problem?" GDS owns the first question. The modeler owns the second.
Layer 1: Generic Checks (G-series)
Generic checks operate on the compiled SystemIR -- the flat block graph with typed wirings. They verify structural topology independent of any domain semantics.
G-004: Dangling Wirings
A wiring references a block that does not exist in the system.
from gds.ir.models import BlockIR, FlowDirection, SystemIR, WiringIR
system = SystemIR(
name="Dangling Wiring Demo",
blocks=[
BlockIR(name="A", signature=("", "Signal", "", "")),
BlockIR(name="B", signature=("Signal", "", "", "")),
],
wirings=[
WiringIR(
source="Ghost", # does not exist!
target="B",
label="signal",
direction=FlowDirection.COVARIANT,
),
],
)
from gds.verification.engine import verify
from gds.verification.generic_checks import check_g004_dangling_wirings
report = verify(system, checks=[check_g004_dangling_wirings])
# -> G-004 FAIL: source 'Ghost' unknown
G-001/G-005: Type Mismatches
Block A outputs Temperature but Block B expects Pressure. The wiring label does not match either side.
system = SystemIR(
name="Type Mismatch Demo",
blocks=[
BlockIR(name="A", signature=("", "Temperature", "", "")),
BlockIR(name="B", signature=("Pressure", "", "", "")),
],
wirings=[
WiringIR(
source="A", target="B",
label="humidity", # matches neither side
direction=FlowDirection.COVARIANT,
),
],
)
- G-001 flags: wiring label does not match source out or target in
- G-005 flags: type mismatch in sequential composition
G-006: Covariant Cycles
Three blocks form a cycle via non-temporal covariant wirings -- an algebraic loop that cannot be resolved within a single timestep.
system = SystemIR(
name="Covariant Cycle Demo",
blocks=[
BlockIR(name="A", signature=("Signal", "Signal", "", "")),
BlockIR(name="B", signature=("Signal", "Signal", "", "")),
BlockIR(name="C", signature=("Signal", "Signal", "", "")),
],
wirings=[
WiringIR(source="A", target="B", label="signal",
direction=FlowDirection.COVARIANT),
WiringIR(source="B", target="C", label="signal",
direction=FlowDirection.COVARIANT),
WiringIR(source="C", target="A", label="signal",
direction=FlowDirection.COVARIANT),
],
)
# -> G-006 FAIL: covariant flow graph contains a cycle
G-003: Direction Contradictions
A wiring marked COVARIANT but also is_feedback=True is a contradiction: feedback implies contravariant flow.
WiringIR(
source="A", target="B",
label="command",
direction=FlowDirection.COVARIANT,
is_feedback=True, # contradiction!
)
# -> G-003 FAIL: COVARIANT + is_feedback contradiction
Fix and Re-verify
The core workflow: build a broken model, run checks, inspect findings, fix errors, re-verify.
from gds.verification.engine import verify
from gds_examples.verification.broken_models import (
dangling_wiring_system,
fixed_pipeline_system,
)
# Step 1: Broken model
broken_report = verify(dangling_wiring_system())
# -> errors >= 1
# Step 2: Fixed model
fixed_report = verify(fixed_pipeline_system())
# -> all checks pass, 0 errors
Layer 2: Semantic Checks (SC-series)
Semantic checks operate on GDSSpec -- the specification registry with types, entities, blocks, and parameters. They verify domain properties like completeness, determinism, and canonical well-formedness.
SC-001: Orphan State Variables
Entity Reservoir has variable level but no mechanism updates it.
from gds.blocks.roles import Policy
from gds.spec import GDSSpec
from gds.state import Entity, StateVariable
from gds.types.interface import Interface, port
from gds.types.typedef import TypeDef
Count = TypeDef(name="Count", python_type=int, constraint=lambda x: x >= 0)
spec = GDSSpec(name="Orphan State Demo")
spec.register_type(Count)
reservoir = Entity(
name="Reservoir",
variables={
"level": StateVariable(name="level", typedef=Count, symbol="L"),
},
)
spec.register_entity(reservoir)
# A policy observes but no mechanism updates the reservoir
observe = Policy(
name="Observe Level",
interface=Interface(forward_out=(port("Level Signal"),)),
)
spec.register_block(observe)
from gds.verification.spec_checks import check_completeness
findings = check_completeness(spec)
# -> SC-001 WARNING: orphan state variable Reservoir.level
SC-002: Write Conflicts
Two mechanisms both update Counter.value within the same wiring -- non-deterministic state transition.
from gds.blocks.roles import BoundaryAction, Mechanism
inc = Mechanism(
name="Increment Counter",
interface=Interface(forward_in=(port("Delta Signal"),)),
updates=[("Counter", "value")],
)
dec = Mechanism(
name="Decrement Counter",
interface=Interface(forward_in=(port("Delta Signal"),)),
updates=[("Counter", "value")], # same variable!
)
from gds.verification.spec_checks import check_determinism
findings = check_determinism(spec)
# -> SC-002 ERROR: write conflict -- Counter.value updated by two mechanisms
A spec with no mechanisms and no entities -- empty state transition and empty state space.
spec = GDSSpec(name="Empty Canonical Demo")
spec.register_block(Policy(
name="Observer",
interface=Interface(
forward_in=(port("Input Signal"),),
forward_out=(port("Output Signal"),),
),
))
from gds.verification.spec_checks import check_canonical_wellformedness
findings = check_canonical_wellformedness(spec)
# -> SC-006 FAIL: no mechanisms found -- state transition f is empty
# -> SC-007 FAIL: state space X is empty
Layer 3: Domain Checks (SF-series)
Domain checks operate on the DSL model before compilation. They catch errors that only make sense in the domain semantics -- for example, "orphan stock" is meaningless outside stock-flow.
The StockFlow DSL provides SF-001..SF-005, running before GDS compilation for early feedback in domain-native terms.
SF-001: Orphan Stocks
A stock has no connected flows -- nothing fills or drains it.
from stockflow.dsl.elements import Flow, Stock
from stockflow.dsl.model import StockFlowModel
model = StockFlowModel(
name="Orphan Stock Demo",
stocks=[
Stock(name="Active"),
Stock(name="Inventory"), # no flows!
],
flows=[
Flow(name="Production", target="Active"),
Flow(name="Consumption", source="Active"),
],
)
from stockflow.verification.checks import check_sf001_orphan_stocks
findings = check_sf001_orphan_stocks(model)
# -> SF-001 WARNING: Stock 'Inventory' has no connected flows
SF-003: Auxiliary Cycles
Circular dependency between auxiliaries -- Price depends on Demand, which depends on Price.
from stockflow.dsl.elements import Auxiliary, Stock
from stockflow.dsl.model import StockFlowModel
model = StockFlowModel(
name="Cyclic Auxiliary Demo",
stocks=[Stock(name="Supply")],
auxiliaries=[
Auxiliary(name="Price", inputs=["Demand"]),
Auxiliary(name="Demand", inputs=["Price"]),
],
)
from stockflow.verification.checks import check_sf003_auxiliary_acyclicity
findings = check_sf003_auxiliary_acyclicity(model)
# -> SF-003 ERROR: cycle detected in auxiliary dependency graph
SF-004: Unused Converters
A converter is declared but no auxiliary reads from it.
from stockflow.dsl.elements import Auxiliary, Converter, Flow, Stock
from stockflow.dsl.model import StockFlowModel
model = StockFlowModel(
name="Unused Converter Demo",
stocks=[Stock(name="Revenue")],
flows=[Flow(name="Income", target="Revenue")],
auxiliaries=[Auxiliary(name="Growth", inputs=["Revenue"])],
converters=[Converter(name="Tax Rate")], # unused!
)
from stockflow.verification.checks import check_sf004_converter_connectivity
findings = check_sf004_converter_connectivity(model)
# -> SF-004 WARNING: Converter 'Tax Rate' is NOT referenced by any auxiliary
Combined Domain + GDS Checks
The StockFlow verification engine can run domain checks (SF) and generic GDS checks (G) together:
from stockflow.verification.engine import verify
report = verify(model, include_gds_checks=True)
sf_findings = [f for f in report.findings if f.check_id.startswith("SF-")]
gds_findings = [f for f in report.findings if f.check_id.startswith("G-")]
Check Reference
Generic Checks (SystemIR)
| ID |
Name |
Catches |
| G-001 |
Domain/codomain matching |
Wiring label vs port mismatch |
| G-002 |
Signature completeness |
Blocks with no ports |
| G-003 |
Direction consistency |
COVARIANT + feedback flag |
| G-004 |
Dangling wirings |
References to missing blocks |
| G-005 |
Sequential type compat |
Mismatched >> port types |
| G-006 |
Covariant acyclicity |
Algebraic loops |
Semantic Checks (GDSSpec)
| ID |
Name |
Catches |
| SC-001 |
Completeness |
Orphan state variables |
| SC-002 |
Determinism |
Write conflicts |
| SC-003 |
Reachability |
Unreachable blocks |
| SC-004 |
Type safety |
TypeDef violations |
| SC-005 |
Parameter refs |
Unregistered params |
| SC-006 |
Canonical f |
No mechanisms |
| SC-007 |
Canonical X |
No state space |
Domain Checks (StockFlowModel)
| ID |
Name |
Catches |
| SF-001 |
Orphan stocks |
Stocks with no flows |
| SF-003 |
Auxiliary cycles |
Circular aux deps |
| SF-004 |
Converter connectivity |
Unused converters |
API Pattern
from gds.verification.engine import verify
system = compile_system(name="My Model", root=pipeline)
report = verify(system)
for finding in report.findings:
print(f"{finding.check_id}: {finding.message}")
Interactive Notebook
Source code for packages/gds-examples/notebooks/verification.py
Tip: paste this code into an empty cell, and the marimo editor will create cells for you
"""GDS Verification Guide — Interactive Marimo Notebook.
Explore the three layers of GDS verification by running checks on
deliberately broken models, inspecting findings, and watching the
fix-and-reverify workflow in action.
Run interactively:
uv run marimo edit notebooks/verification.py
Run as read-only app:
uv run marimo run notebooks/verification.py
"""
# /// script
# requires-python = ">=3.12"
# dependencies = [
# "gds-examples",
# "marimo>=0.20.0",
# ]
# ///
import marimo
__generated_with = "0.20.2"
app = marimo.App(width="medium", app_title="GDS Verification Guide")
# ── Setup ────────────────────────────────────────────────────
@app.cell
def imports():
import marimo as mo
return (mo,)
@app.cell
def header(mo):
mo.md(
"""
# GDS Verification Guide
GDS has **three layers** of verification checks, each operating
on a different representation:
| Layer | Checks | Operates on | Catches |
|-------|--------|-------------|---------|
| Generic | G-001..G-006 | `SystemIR` | Structural topology errors |
| Semantic | SC-001..SC-007 | `GDSSpec` | Domain property violations |
| Domain | SF-001..SF-005 | DSL model | DSL-specific errors |
This notebook walks through each layer with deliberately broken
models, showing what each check detects and how to fix it.
"""
)
return ()
# ── Section 1: Generic Checks ───────────────────────────────
@app.cell
def section_generic_header(mo):
mo.md(
"""
---
## Section 1: Generic Checks (G-series)
Generic checks operate on the compiled `SystemIR` — the flat
block graph with typed wirings. They verify **structural
topology** independent of any domain semantics.
Select a broken model below to see which check catches the error.
"""
)
return ()
@app.cell
def generic_selector(mo):
generic_dropdown = mo.ui.dropdown(
options={
"G-004: Dangling Wiring": "dangling",
"G-001/G-005: Type Mismatch": "type_mismatch",
"G-006: Covariant Cycle": "cycle",
"G-003: Direction Contradiction": "direction",
"G-002: Incomplete Signature": "signature",
},
value="G-004: Dangling Wiring",
label="Broken model",
)
return (generic_dropdown,)
@app.cell
def run_generic_check(mo, generic_dropdown):
from gds_examples.verification.broken_models import (
covariant_cycle_system,
dangling_wiring_system,
direction_contradiction_system,
incomplete_signature_system,
type_mismatch_system,
)
from gds.verification.engine import verify
from gds.verification.generic_checks import (
check_g001_domain_codomain_matching,
check_g002_signature_completeness,
check_g003_direction_consistency,
check_g004_dangling_wirings,
check_g005_sequential_type_compatibility,
check_g006_covariant_acyclicity,
)
_models = {
"dangling": (
dangling_wiring_system,
[check_g004_dangling_wirings],
"A wiring references block **'Ghost'** which doesn't exist. "
"G-004 checks that every wiring source and target names a "
"real block in the system.",
),
"type_mismatch": (
type_mismatch_system,
[
check_g001_domain_codomain_matching,
check_g005_sequential_type_compatibility,
],
"Block A outputs **'Temperature'** but Block B expects "
"**'Pressure'**. The wiring label 'humidity' matches "
"neither. G-001 checks label/port matching; G-005 checks "
"sequential type compatibility.",
),
"cycle": (
covariant_cycle_system,
[check_g006_covariant_acyclicity],
"Blocks A → B → C → A form a **covariant "
"cycle** — an algebraic loop within a single timestep. "
"G-006 checks that the covariant flow graph is acyclic.",
),
"direction": (
direction_contradiction_system,
[check_g003_direction_consistency],
"A wiring is marked **COVARIANT** but also "
"**is_feedback=True** — a contradiction, since feedback "
"implies contravariant flow. G-003 catches this.",
),
"signature": (
incomplete_signature_system,
[check_g002_signature_completeness],
"Block **'Orphan'** has a completely empty signature — "
"no forward or backward ports at all. G-002 flags blocks "
"with no inputs and no outputs.",
),
}
_model_fn, _checks, _description = _models[generic_dropdown.value]
_system = _model_fn()
_report = verify(_system, checks=_checks)
_failures = [f for f in _report.findings if not f.passed]
_passes = [f for f in _report.findings if f.passed]
_findings_rows = []
for _f in _report.findings:
_icon = "PASS" if _f.passed else "FAIL"
_findings_rows.append(
f"| {_icon} | {_f.check_id} | {_f.severity.name} | {_f.message} |"
)
_findings_table = (
"| Status | Check | Severity | Message |\n"
"|--------|-------|----------|---------|\n" + "\n".join(_findings_rows)
)
mo.vstack(
[
mo.md(f"### {_system.name}\n\n{_description}"),
mo.md(f"**Results:** {len(_passes)} passed, {len(_failures)} failed"),
mo.md(_findings_table),
]
)
return ()
# ── Fix and Re-verify ────────────────────────────────────────
@app.cell
def fix_reverify_header(mo):
mo.md(
"""
---
### Fix and Re-verify
The core workflow: build a broken model, run checks, inspect
findings, fix the errors, re-verify. Below we compare the
dangling-wiring system against its fixed counterpart.
"""
)
return ()
@app.cell
def fix_reverify_demo(mo):
from gds_examples.verification.broken_models import (
dangling_wiring_system as _dangling_wiring_system,
)
from gds_examples.verification.broken_models import (
fixed_pipeline_system,
)
from gds.verification.engine import verify as _verify
_broken_report = _verify(_dangling_wiring_system())
_fixed_report = _verify(fixed_pipeline_system())
_broken_failures = [f for f in _broken_report.findings if not f.passed]
_fixed_failures = [f for f in _fixed_report.findings if not f.passed]
mo.hstack(
[
mo.vstack(
[
mo.md(
"**Broken** (dangling wiring)\n\n"
f"- Checks: {_broken_report.checks_total}\n"
f"- Errors: {_broken_report.errors}\n"
f"- Passed: {_broken_report.checks_passed}"
),
mo.md(
"\n".join(
f"- **{f.check_id}**: {f.message}" for f in _broken_failures
)
or "*(no failures)*"
),
]
),
mo.vstack(
[
mo.md(
"**Fixed** (clean pipeline)\n\n"
f"- Checks: {_fixed_report.checks_total}\n"
f"- Errors: {_fixed_report.errors}\n"
f"- Passed: {_fixed_report.checks_passed}"
),
mo.md(
"\n".join(
f"- **{f.check_id}**: {f.message}" for f in _fixed_failures
)
or "All checks passed."
),
]
),
],
widths="equal",
)
return ()
# ── Section 2: Semantic Checks ──────────────────────────────
@app.cell
def section_semantic_header(mo):
mo.md(
"""
---
## Section 2: Semantic Checks (SC-series)
Semantic checks operate on `GDSSpec` — the specification
registry with types, entities, blocks, and parameters. They
verify **domain properties** like completeness, determinism,
and canonical well-formedness.
These are complementary to generic checks: a model can pass
all G-checks but fail SC-checks (and vice versa).
"""
)
return ()
@app.cell
def semantic_selector(mo):
semantic_dropdown = mo.ui.dropdown(
options={
"SC-001: Orphan State Variable": "orphan",
"SC-002: Write Conflict": "conflict",
"SC-006/007: Empty Canonical": "empty",
},
value="SC-001: Orphan State Variable",
label="Broken spec",
)
return (semantic_dropdown,)
@app.cell
def run_semantic_check(mo, semantic_dropdown):
from gds_examples.verification.broken_models import (
empty_canonical_spec,
orphan_state_spec,
write_conflict_spec,
)
from gds.verification.spec_checks import (
check_canonical_wellformedness,
check_completeness,
check_determinism,
)
_specs = {
"orphan": (
orphan_state_spec,
check_completeness,
"Entity **Reservoir** has variable `level` but no "
"mechanism updates it. SC-001 flags this as a **WARNING** "
"— the state variable is structurally orphaned.",
),
"conflict": (
write_conflict_spec,
check_determinism,
"Two mechanisms both update `Counter.value` within the "
"same wiring. SC-002 flags this as an **ERROR** — the "
"state transition is non-deterministic.",
),
"empty": (
empty_canonical_spec,
check_canonical_wellformedness,
"A spec with no mechanisms and no entities. SC-006 flags "
"the empty state transition (f is empty); SC-007 flags "
"the empty state space (X is empty).",
),
}
_spec_fn, _check_fn, _description = _specs[semantic_dropdown.value]
_spec = _spec_fn()
_findings = _check_fn(_spec)
_failures = [f for f in _findings if not f.passed]
_passes = [f for f in _findings if f.passed]
_rows = []
for _f in _findings:
_icon = "PASS" if _f.passed else "FAIL"
_rows.append(f"| {_icon} | {_f.check_id} | {_f.severity.name} | {_f.message} |")
_table = (
"| Status | Check | Severity | Message |\n"
"|--------|-------|----------|---------|\n" + "\n".join(_rows)
)
mo.vstack(
[
mo.md(f"### {_spec.name}\n\n{_description}"),
mo.md(f"**Results:** {len(_passes)} passed, {len(_failures)} failed"),
mo.md(_table),
]
)
return ()
# ── Generic vs Semantic Comparison ───────────────────────────
@app.cell
def comparison_header(mo):
mo.md(
"""
---
### Generic vs Semantic: Complementary Layers
A well-formed model must pass **both** layers. Below we run
both on the fixed model to confirm they are complementary.
"""
)
return ()
@app.cell
def comparison_demo(mo):
from gds_examples.verification.verification_demo import (
demo_generic_vs_semantic,
)
_results = demo_generic_vs_semantic()
_generic = _results["generic"]
_semantic = _results["semantic"]
mo.hstack(
[
mo.vstack(
[
mo.md(
"**Generic (G-series)**\n\n"
f"- Total: {_generic.checks_total}\n"
f"- Passed: {_generic.checks_passed}\n"
f"- Errors: {_generic.errors}"
),
]
),
mo.vstack(
[
mo.md(
"**Semantic (SC-series)**\n\n"
f"- Total: {_semantic.checks_total}\n"
f"- Passed: {_semantic.checks_passed}\n"
f"- Errors: {_semantic.errors}"
),
]
),
],
widths="equal",
)
return ()
# ── Section 3: Domain Checks ────────────────────────────────
@app.cell
def section_domain_header(mo):
mo.md(
"""
---
## Section 3: Domain Checks (SF-series)
Domain checks operate on the **DSL model** before compilation.
They catch errors that only make sense in the domain semantics
— e.g., "orphan stock" is meaningless outside stock-flow.
The StockFlow DSL provides SF-001..SF-005. These run before
GDS compilation, giving early feedback in domain-native terms.
"""
)
return ()
@app.cell
def domain_selector(mo):
domain_dropdown = mo.ui.dropdown(
options={
"SF-001: Orphan Stock": "orphan",
"SF-003: Auxiliary Cycle": "cycle",
"SF-004: Unused Converter": "converter",
},
value="SF-001: Orphan Stock",
label="Broken model",
)
return (domain_dropdown,)
@app.cell
def run_domain_check(mo, domain_dropdown):
from gds_examples.verification.domain_checks_demo import (
cyclic_auxiliary_model,
orphan_stock_model,
unused_converter_model,
)
from stockflow.verification.checks import (
check_sf001_orphan_stocks,
check_sf003_auxiliary_acyclicity,
check_sf004_converter_connectivity,
)
_models = {
"orphan": (
orphan_stock_model,
check_sf001_orphan_stocks,
"Stock **'Inventory'** has no connected flows — nothing "
"fills or drains it. SF-001 flags this as a WARNING.",
),
"cycle": (
cyclic_auxiliary_model,
check_sf003_auxiliary_acyclicity,
"Auxiliary **'Price'** depends on 'Demand', which depends "
"on 'Price' — a circular dependency. SF-003 flags this "
"as an ERROR.",
),
"converter": (
unused_converter_model,
check_sf004_converter_connectivity,
"Converter **'Tax Rate'** is declared but no auxiliary "
"reads from it. SF-004 flags this as a WARNING.",
),
}
_model_fn, _check_fn, _description = _models[domain_dropdown.value]
_model = _model_fn()
_findings = _check_fn(_model)
_failures = [f for f in _findings if not f.passed]
_passes = [f for f in _findings if f.passed]
_rows = []
for _f in _findings:
_icon = "PASS" if _f.passed else "FAIL"
_rows.append(f"| {_icon} | {_f.check_id} | {_f.severity.name} | {_f.message} |")
_table = (
"| Status | Check | Severity | Message |\n"
"|--------|-------|----------|---------|\n" + "\n".join(_rows)
)
mo.vstack(
[
mo.md(f"### {_model.name}\n\n{_description}"),
mo.md(f"**Results:** {len(_passes)} passed, {len(_failures)} failed"),
mo.md(_table),
]
)
return ()
# ── Domain + GDS Combined ───────────────────────────────────
@app.cell
def combined_header(mo):
mo.md(
"""
---
### Domain + GDS: Full Verification Stack
The StockFlow verification engine can run domain checks (SF)
**and** generic GDS checks (G) together. Toggle below to
see how a good model passes both, while a broken model shows
failures at the domain layer alongside GDS results.
"""
)
return ()
@app.cell
def combined_selector(mo):
combined_dropdown = mo.ui.dropdown(
options={
"Good Model (Population)": "good",
"Broken Model (Orphan Stock)": "broken",
},
value="Good Model (Population)",
label="Model",
)
return (combined_dropdown,)
@app.cell
def run_combined(mo, combined_dropdown):
from gds_examples.verification.domain_checks_demo import (
good_stockflow_model,
)
from gds_examples.verification.domain_checks_demo import (
orphan_stock_model as _orphan_stock_model,
)
from stockflow.verification.engine import verify as sf_verify
if combined_dropdown.value == "good":
_model = good_stockflow_model()
else:
_model = _orphan_stock_model()
_report = sf_verify(_model, include_gds_checks=True)
_sf = [f for f in _report.findings if f.check_id.startswith("SF-")]
_gds = [f for f in _report.findings if f.check_id.startswith("G-")]
_sf_fail = [f for f in _sf if not f.passed]
_gds_fail = [f for f in _gds if not f.passed]
mo.hstack(
[
mo.vstack(
[
mo.md(
f"**Domain (SF)** — {len(_sf)} checks, {len(_sf_fail)} failures"
),
mo.md(
"\n".join(
f"- {'FAIL' if not f.passed else 'PASS'} "
f"**{f.check_id}**: {f.message}"
for f in _sf
)
or "*(no SF checks)*"
),
]
),
mo.vstack(
[
mo.md(
f"**Generic (G)** — {len(_gds)} checks, "
f"{len(_gds_fail)} failures"
),
mo.md(
"\n".join(
f"- {'FAIL' if not f.passed else 'PASS'} "
f"**{f.check_id}**: {f.message}"
for f in _gds
)
or "*(no G checks)*"
),
]
),
],
widths="equal",
)
return ()
# ── Reference ────────────────────────────────────────────────
@app.cell
def reference(mo):
mo.md(
"""
---
## Check Reference
### Generic Checks (SystemIR)
| ID | Name | Catches |
|----|------|---------|
| G-001 | Domain/codomain matching | Wiring label vs port mismatch |
| G-002 | Signature completeness | Blocks with no ports |
| G-003 | Direction consistency | COVARIANT + feedback flag |
| G-004 | Dangling wirings | References to missing blocks |
| G-005 | Sequential type compat | Mismatched >> port types |
| G-006 | Covariant acyclicity | Algebraic loops |
### Semantic Checks (GDSSpec)
| ID | Name | Catches |
|----|------|---------|
| SC-001 | Completeness | Orphan state variables |
| SC-002 | Determinism | Write conflicts |
| SC-003 | Reachability | Unreachable blocks |
| SC-004 | Type safety | TypeDef violations |
| SC-005 | Parameter refs | Unregistered params |
| SC-006 | Canonical f | No mechanisms |
| SC-007 | Canonical X | No state space |
### Domain Checks (StockFlowModel)
| ID | Name | Catches |
|----|------|---------|
| SF-001 | Orphan stocks | Stocks with no flows |
| SF-003 | Auxiliary cycles | Circular aux deps |
| SF-004 | Converter connectivity | Unused converters |
### API Pattern
```python
from gds.verification.engine import verify
system = compile_system(name="My Model", root=pipeline)
report = verify(system)
for finding in report.findings:
print(f"{finding.check_id}: {finding.message}")
```
"""
)
return ()
if __name__ == "__main__":
app.run()
To run the notebook locally:
uv run marimo run packages/gds-examples/notebooks/verification.py
Run the test suite:
uv run --package gds-examples pytest packages/gds-examples/tests/test_verification_guide.py -v
Source Files