feat: formal verification framework + StateMetric (bridge Step 3)

.github/workflows/ci.yml

@@ -32,6 +32,8 @@ jobs:
       - uses: astral-sh/setup-uv@v7
       - run: uv sync --package ${{ matrix.package }}
       - name: Run tests
+        env:
+          HYPOTHESIS_PROFILE: ci
         run: |
           if [ "${{ matrix.package }}" = "gds-examples" ]; then
             uv run --package ${{ matrix.package }} pytest packages/gds-examples -v

docs/guides/dsl-roadmap.md

@@ -90,7 +90,7 @@ From the architecture document — these are non-negotiable:
 
 ## Open Research Directions
 
-See [Research Boundaries and Open Questions](research-boundaries.md) for detailed analysis of:
+See [Research Boundaries and Open Questions](../research/research-boundaries.md) for detailed analysis of:
 
 1. **MIMO semantics** — scalar ports vs vector-valued spaces
 2. **Timestep semantics** — what `.loop()` means across DSLs when execution is introduced

docs/guides/interoperability.md

@@ -179,7 +179,7 @@ Three layers of simulation logic, each consuming only `get_payoff()`:
 Each layer is independently testable. The simulation code knows nothing about OGS composition trees, PatternIR, or GDS blocks — it only knows payoff values.
 
 !!! note "Thin runner, not a general simulator"
-    This is **not** a GDS execution engine. It is a domain-specific simulation that uses the GDS specification as its source of truth for game rules. The strategies, match logic, and evolutionary dynamics are all hand-written Python specific to the iterated PD. A general `gds-sim` would require solving the much harder problem of executing arbitrary GDS specifications — see [Research Boundaries](research-boundaries.md#research-question-2-what-does-a-timestep-mean-across-dsls).
+    This is **not** a GDS execution engine. It is a domain-specific simulation that uses the GDS specification as its source of truth for game rules. The strategies, match logic, and evolutionary dynamics are all hand-written Python specific to the iterated PD. A general `gds-sim` would require solving the much harder problem of executing arbitrary GDS specifications — see [Research Boundaries](../research/research-boundaries.md#research-question-2-what-does-a-timestep-mean-across-dsls).
 
 ---
 
@@ -290,7 +290,7 @@ All paths relative to `packages/gds-examples/`.
 
 ## Connection to Research Boundaries
 
-This work provides concrete evidence for two open questions in [Research Boundaries](research-boundaries.md):
+This work provides concrete evidence for two open questions in [Research Boundaries](../research/research-boundaries.md):
 
 **RQ2 (Timestep semantics):** The tournament simulator implements a specific execution model — synchronous iterated play with optional noise — on top of a structural specification that encodes no execution semantics. This is exactly the pattern anticipated in RQ2: "Each DSL defines its own execution contract if/when it adds simulation."
 

docs/guides/view-stratification.md

@@ -127,8 +127,8 @@ canonical, they must augment it with execution semantics from the domain
 layer. Canonical alone is insufficient for execution. This boundary must
 remain explicit to avoid the illusion that `h = f ∘ g` is a runnable program.
 
-See [RQ2 (timestep semantics)](research-boundaries.md#research-question-2-what-does-a-timestep-mean-across-dsls)
-and [RQ4 (cross-lens analysis)](research-boundaries.md#research-question-4-cross-lens-analysis-when-equilibrium-and-reachability-disagree).
+See [RQ2 (timestep semantics)](../research/research-boundaries.md#research-question-2-what-does-a-timestep-mean-across-dsls)
+and [RQ4 (cross-lens analysis)](../research/research-boundaries.md#research-question-4-cross-lens-analysis-when-equilibrium-and-reachability-disagree).
 
 ### Semantic enrichment must remain opt-in
 

docs/owl/guide/representability.md

@@ -2,7 +2,7 @@
 
 The formal representability analysis classifies which GDS concepts can and cannot be represented in OWL/SHACL/SPARQL.
 
-See the full analysis: [formal-representability.md](https://github.com/BlockScience/gds-core/blob/dev/packages/gds-owl/docs/formal-representability.md)
+See the full analysis: [formal-representability.md](../../research/formal-representability.md)
 
 ## Key Results