The Four-Boundary Spec Mapping
Where the corpus already does message / composition / interop / render, and where the field has tooling vs. where it doesn't
Table of Contents
1. The four boundary types
This note takes a four-row classification of cross-boundary specification tooling and maps it onto the existing corpus. The classification is not ours – it was derived from a survey of three industrial+academic communities (contract testers, session-types theorists, standards-body conformance teams) that do not cite each other and yet built separate machinery for the same shape.
| # | Boundary | Tool family | What it verifies |
|---|---|---|---|
| 1 | message | Pact / Pactflow bidirectional, Prism, Microcks | each side vs. a shared artifact (OpenAPI, JSON Schema) |
| 2 | composition | MPST / Scribble, Session*/F*, TLA+, Dafny | global protocol projects to a local type; refinements typed on each role |
| 3 | interop (incl. browser↔localhost) | OpenID / FIDO conformance suites | the suite plays the missing party; dev-vs-cert split |
| 4 | render | (nothing) – only snapshot / visual-regression | "matches the recording I took," not "satisfies an invariant" |
The interesting fact about the classification: rows 1–3 are well-tooled, three different ways, from three communities that don't read each other's papers. Row 4 has nothing purpose-built. The corpus had already located that gap independently before this taxonomy arrived; why-this-is-hard names it as the open problem.
The corpus's coverage, mapped to the four rows:
| # | Boundary | Notes in corpus | Density |
|---|---|---|---|
| 1 | message | ~14 | high |
| 2 | composition | ~14 | high |
| 3 | interop | ~5 | medium |
| 4 | render | ~9 (all critiquing the absence) | high as critique, none as solution |
That is the corpus's situation in one table: rows 1–3 have multiple notes each grounding industry tooling; row 4 has multiple notes all saying the same thing – there is no tool – and proposing partial, hand-rolled answers (Goldberry catalog, Bombadil LTL, ARIA APG patterns).
2. Boundary 1: message
Verifies: that two independently built endpoints, one of which may be uncontrollable in test (a public API, a deployed dashboard), satisfy the same shared artifact without ever running against each other.
Industry tooling: Pact + Pactflow bidirectional, Prism (Stoplight), Microcks, OpenAPI codegen, Apicurio.
2.1. Corpus notes that ground the message boundary
| Note | Concept it grounds |
|---|---|
| Design-Driven APIs | OpenAPI-first design, Prism mock servers, Dredd contract testing |
| API Development with Swagger | Swagger/OpenAPI as documentation + contract + mock |
| JSON Schema for Polyglot Engineers | schema-as-artifact across Haskell, TypeScript, Clojure, Python |
| Incremental Rails to SPA Migration with Mock APIs | contract-driven decoupling, Swagger as the migration spine |
| SPA Setup with Rails: JSON:API and Angular | JSON:API spec as the document-shape contract |
| clojure.spec | composable schema definitions; validation/conformance/explanation/generation from one spec |
| Scheme LLM Toolkit | Racket-style contracts that bridge to TLA+, Lean4, OpenAPI |
| Federation Technologies for API Management | Apicurio, SwaggerHub, Stoplight – OpenAPI as governance artifact |
| pocket-es Component Contract Specification | six boundaries with pre/postconditions; search-index.json as shared artifact |
| pocket-es Structured Query Surface | malli + JSON-Schema; single IR as source of truth |
| GraphQL | schema as the shared message contract; federation across subgraphs |
| Lacinia (Clojure GraphQL) | EDN schema as data contract, resolvers validate field shapes |
| Production-Ready GraphQL | schema-first vs. code-first; schema metadata as governance |
| Data Layer Schema | one logical entity expressed across JSON Schema, SQL DDL, Avro, Protobuf |
| Code Generation | protobuf, OpenAPI, GraphQL codegen + LLM-driven synthesis |
2.2. Concept density
The message boundary is the corpus's most thoroughly covered. Fifteen notes, spanning ~10 years of practice, all converging on the same shape: one schema artifact, two implementations checked against it independently. The Pactflow-bidirectional pattern is implicit in nearly all of them; what is missing from the corpus is a note that names the bidirectional pattern as the structural answer to "the deployed consumer is uncontrollable in test."
The Scheme LLM Toolkit is the bridge to row 2: contracts that are message-bounded at the wire but compile to TLA+/Lean4 artifacts that are composition-bounded.
3. Boundary 2: composition
Verifies: that a global protocol projects to a local type per participant, and each participant's process is independently type-checked against its local type. The composed system is then disciplined by the global type without ever being composed in a test.
Industry tooling: Multiparty Session Types (MPST) + Scribble + Session*/F* on the protocol side; TLA+ and Dafny on the verified-state side; choreographic programming (Choral, HasChor) as the endpoint-projection family.
3.1. Corpus notes that ground the composition boundary
| Note | Concept it grounds |
|---|---|
| CP 2026: Choreographic Programming | endpoint projection (EPP), Choral, HasChor; correct-by-construction composition |
| TLA+ for System Design | state-machine modeling for distributed protocols; temporal logic for design validation |
| E-Commerce Order State Machine in TLA+ | concrete state-machine spec; what the global protocol looks like in TLA+ |
| Dafny ↔ Clojure interop | verified round-trip (encode/decode) compiled to JVM bytecode; closes proof-execution gap |
| Dafny spec → clojure.spec Transpiler | refinement schemas from requires~/~ensures; boundary validation where verified meets untrusted |
| Dafny Effects Bridge | Dafny modifies → Clojure ownership (atoms, core.async); effect-safe composition |
| Type Systems: One Tool, Four Ways | TypeScript / Rust / Dafny / Racket on the same reversible-codec spec |
| Dafny 2026 @ POPL | auto-active verification of reversible transducers; reverse ∘ reverse = id as composition property |
| Time-Travel Chat: First-Principles Spec | fork-contract spec with tool-balanced turn boundaries; DAG fork + merge proven via P1–P6b |
| Alloy Specification | relational logic for structural composition; bounded model checking vs. TLA+ temporal |
| defverified: Inline Dafny Macros for Clojure | refinement-typed function bodies live inside Clojure; specification as macro |
| Formal Verification of Transformer Architectures in Rocq | architecture-level composition properties verified in Rocq |
| TLA+ Community Event @ ETAPS 2025 | tooling + case studies grounding the row |
| PaGE 2026 — Shan Lu keynote | LLM agents emit Verus proofs against human specs; spec as TCB for distributed-system composition |
3.2. What's missing
The corpus has no note on multiparty session types or Scribble specifically – the cp-2026 CFP coverage is the closest. This is a visible gap given how much TLA+ and Dafny material the corpus already carries: MPST is the formal frame that would unify the wire-shape work (row 1) with the protocol-state work (this row). Filing as follow-up work.
4. Boundary 3: interop (no-channel, incl. browser↔localhost)
Verifies: when a side cannot be co-deployed with its counterpart (because the counterpart is a browser, or a public service, or a deployed certifying instance), a conformance suite plays the missing party. Structural feature: a dev-vs-cert split – you may run a local instance for development, you must use the hosted instance for certification.
Industry tooling: OpenID Foundation conformance suite, FIDO Alliance conformance tool, and the long line of W3C conformance test suites. Adjacent: deterministic simulation testing (Antithesis), property-based testing harnesses (Bombadil) on the verification side.
4.1. Corpus notes that ground the interop boundary
| Note | Concept it grounds |
|---|---|
| crowsnest v2.1 Specification | HATEOAS service index + /openapi.json as receiver-served codegen artifact; fixture-driven conformance F1–F5; deployed dashboard as certifying instance |
| Testing pocket-es from the Outside | phased rollout with per-mechanism gates (unit / test.check / Bombadil / manual) |
| pocket-es Query Surface Rollout | malli-backed contract + test.check properties + Bombadil LTL invariants; conformance-as-phase |
| WWN Test Procedures | state-machine conformance fixtures; boundary at w=±8191; ring-wrap behavior |
| Agent Sandbox Architectures | the proxy-as-counterpart pattern; egress harness as the conformance gate |
4.2. What's missing
The corpus has no note explicitly framing the OpenID / FIDO conformance-suite pattern as the prior art for the crowsnest conformance fixtures or the pocket-es phased rollout. Both are doing the OpenID-suite move; neither names it. The sandbox systems note's "egress proxy as chokepoint" is the same structural move on a different boundary (capability harness, not protocol harness).
The dev-vs-cert split in crowsnest's spec (
site/tools/crowsnest/spec.org, "open https://wal.sh/tools/crowsnest/
in Chrome – this is the real acceptance test") is exactly the FIDO
governance pattern, but isn't named as such. The
crowsnest v3 speculation in _drafts/
proposes to lift it out as the I2 governance section.
5. Boundary 4: render
Verifies: the dashboard / UI renders correctly against an invariant (not a recording). The four-row table's empty cell.
Industry tooling: nothing purpose-built. Snapshot / visual-regression tools (Chromatic, Percy, Playwright snapshots) verify "matches the last recording," which is not an invariant; an uncontracted UI declared no invariant to violate. The nearest formal frame is model-based UI testing – project a state machine, check the UI against it – which is niche precisely because almost no UI ships the model.
5.1. Corpus notes that ground the render boundary
Mostly as the open problem, not as a solution.
| Note | Concept it grounds |
|---|---|
| Goldberry: Frontend Invariant Catalog for DST Harnesses | 10-cluster taxonomy (temporality, totality, boundaries, focus_state, event_graph, lifecycle, layout_contract, a11y_contract, device_contract, security_contract) |
| Goldberry: Why This Is Hard | the 12-layer web contract stack; why unified-contract approaches failed (Closure, Bazel, Phoenix/LiveView); the SARIF analogy |
| Goldberry: Related Work — UI Invariant Specification Landscape | WCAG/ARIA APG, Radix/Headless/React Aria, XState/Harel statecharts, Devcards, 1990s formal methods (Z, VDM, CSP, Interactors) |
| Goldberry: Claims Verification | adversarial review – WCAG covers only 1 of 10 clusters; XState framing precision; Devcards cartesian product |
| Goldberry: Historical UI Systems | 40-year genealogy; invariants the 1980s solved that the web reintroduced (namespace isolation, focus immutability, monotonic z-order) |
| Goldberry: Foundation — Web Platform Timeline | invariants across eras E0–E3; CSS @layer, React Hooks, framework eras |
| Bombadil for SPAs: Property-Based Testing Best Practices | DOM extractors, headless-vs-real-browser divergence, trace-based reproduction; LTL render properties |
| pocket-es Query Surface Rollout | INV-1..9; Bombadil LTL (mode exclusivity, bounded results, error visibility, no auto-translation) |
| WWN Winding Visualization | render contract for the winding-number visualization; state machine on the topology |
5.2. The empty cell is the corpus's clearest agreement
Every one of these notes, independently, names the same gap: the render boundary has no industrial tool that asserts invariants rather than recordings. Goldberry's why-this-is-hard is the most explicit:
Snapshot tools say "matches what I recorded." That's recording, not contract. An uncontracted UI has no invariant to violate.
Bombadil and the pocket-es rollout are the corpus's partial answers: LTL properties checked over a DOM extractor are render-contract approximations. They cover totality, mode exclusivity, ordering, and error visibility but cannot cover layout, focus, or pixel-level invariants in the general case. The Goldberry catalog is the taxonomy of what an industrial render-conformance suite would need to check, and the absence of a tool that implements it is exactly the empty cell.
6. Cross-cutting threads
6.1. Thread A: the OpenAPI-as-pact promotion
Row 1 and Row 3 connect through /openapi.json. The
crowsnest v2.1 spec already serves
it as an additive feature; the
v3
speculation in _drafts/ proposes promoting it to the normative shared
artifact (the Pactflow-bidirectional move) and adding GET /conformance
so the receiver self-reports against its own fixtures (the FIDO move).
The same promotion logic applies to
pocket-es: search-index.json is
already the shared artifact, contracts.org already names the six
boundaries, and query-surface-rollout already does the phased
conformance with Bombadil. The pattern is consistent across the corpus
– it just hasn't been named.
6.2. Thread B: refinement types as the bridge between message and composition
The corpus's heaviest formal-methods cluster – defverified, dafny-clj- interop, dafny-spec-transpiler, dafny-effects-bridge, defverified-macro – is doing exactly what Session*/F* does for MPST: lifting value- constraint refinements from message-bounded contracts (clojure.spec / malli / JSON Schema) into composition-bounded proofs (Dafny / Lean4 / Rocq).
The type- systems note is the corpus's direct comparison across the four type disciplines on the same reversible-codec spec. Adding a fifth column for refinement-typed MPST (Session*/F* or refinement-Scribble) would close the loop.
6.3. Thread C: the conformance-suite pattern is reinvented per-boundary
- crowsnest's F1–F5 fixtures +
--selftest→ OpenID/FIDO suite shape on the protocol boundary. - pocket-es's phased rollout → conformance suite shape on the search-engine boundary.
- 2026-agent-sandbox-systems's egress proxy → conformance suite shape on the capability boundary.
- Bombadil + Goldberry → conformance suite shape on the render boundary (with the caveat that the tool is partial because the boundary has no industry answer).
Four boundaries, four implementations of the same pattern, no shared vocabulary across them. Naming "conformance suite" as a style, the way Antithesis names DST, would let the corpus refactor toward a shared harness shape.
7. The mapping table, condensed
| Corpus cluster | Boundary | Tool family analogue |
|---|---|---|
| OpenAPI / Swagger / JSON Schema / GraphQL notes (15) | message | Pact / Pactflow bidirectional, Prism, Microcks |
| TLA+ + Dafny + Lean + Rocq + Alloy notes (14) | composition | MPST / Scribble, Session*/F* |
| crowsnest spec + pocket-es rollout + WWN testing + sandbox proxy | interop | OpenID / FIDO conformance suite |
| Goldberry catalog + Bombadil + WWN viz (9) | render | (no industry tool; snapshot is insufficient) |
8. Refutation conditions
This mapping is wrong, and this note must be revised, if:
- A corpus note exists that explicitly names the bidirectional-pact pattern and I missed it. (Means the message-boundary coverage is even higher than reported.)
- A corpus note exists that uses Scribble or refinement-MPST specifically and I missed it. (Means the composition-boundary gap is smaller than reported.)
- An industrial tool exists for the render boundary that asserts invariants (not recordings) and the corpus has not located it. (Means row 4's empty cell is wrong.)
- The four-row classification itself is wrong – there is a fifth boundary the corpus already covers, or row 3 (interop) is really two rows. (Means the taxonomy needs revisiting.)
9. Open questions
- Is a single mapping note enough, or should the four boundaries get
sibling notes –
message-boundary-notes,composition-boundary- notes, etc. – each indexing its row? Argument for siblings: each row deserves its own table-of-contents view. Argument against: the cross-boundary threads above are the actual contribution; siblings would lose them. - Should the absent MPST/Scribble note be commissioned as new work, or is the choreographic-programming coverage sufficient? CP and MPST are close cousins but not the same.
- Does
crowsnest v3(the _drafts/ speculation) become a published research note once the bidirectional-pact promotion lands in v2.1, or does it remain a spec pinned to the tool? Probably the former; the four-row framing is research, the receiver bytes are specification.
10. References
External:
- Pact / Pactflow bidirectional –
https://pactflow.io/ - Prism (Stoplight) – OpenAPI-driven mock server
- Microcks – OpenAPI / AsyncAPI conformance + mocking
- Multiparty Session Types (Honda / Yoshida / Carbone)
- Scribble – MPST toolchain
- Session*/F* (Castro-Perez et al.) – refinement-typed multiparty
- OpenID Foundation Conformance Suite
- FIDO Alliance Conformance Tools
- Antithesis – deterministic simulation testing
- Bombadil – LTL-based property testing for SPAs
Internal (the boundary-typed corpus):
- Message: design-driven-apis, swagger, json-schema, api-mock, jsonapi-rails-angularjs, clojure.spec, 2025-scheme-llm-toolkit, federation, pocket-es/contracts, pocket-es/query-surface-spec, graphql, clojure-graphql, production-ready-graphql, datalayer-schema, generating-code.
- Composition: events/pldi-2026/cp-2026, tla-plus-system-design, dafny-clj-interop, dafny-spec-transpiler, dafny-effects-bridge, 2026-type-systems-one-tool-four-ways, events/popl26/dafny-2026, 2026-repl-driven-chat-mutation/spec, 2026-alloy-specification, defverified-macro, 2025-formal-transformer-verification, events/tla-etaps-2025, events/pldi-2026/page-2026/keynote-shan-lu.
- Interop: tools/crowsnest/spec, pocket-es/verification, pocket-es/query-surface-rollout, wwn/testing, 2026-agent-sandbox-systems.
- Render: 2026-goldberry-frontend-invariants (and its includes: why-this-is-hard, related-work, claims-verification, historical-ui-systems, foundation), bombadil-spa, pocket-es/query-surface-rollout, wwn/viz.