Literate AI

Repository documentation

SCXML specification_provider — design spike (MEDIUM(c))

This is not committed 0.5.0 scope

This document is the design spike docs/roadmap/0.5.0-specification-hierarchy.md's MEDIUM(c) breakdown calls for — it exists so a future SCXML specification_provider can be scoped precisely before any code is written. Nothing in this document is promised 0.5.0 delivery. See 0.5.0-scope.md for what is actually committed this cycle, and 0.5.0-specification-hierarchy.md for why MEDIUM(a)/(b)/(c)/LOW are planning, not commitments. A sibling design spike for MEDIUM(b) (DMN) is running concurrently on this same branch; where this document's answer to a shared question is identical to what DMN would need, it says so explicitly rather than re-deriving it.

The problem, in one sentence

OpenSpec's WHEN/THEN format is a poor fit for state-machine/protocol/workflow logic — the issue underlying 0.5.0-specification-hierarchy.md expects this to be the common case among Components with state-machine-shaped behavior — and SCXML (the W3C State Chart XML standard) is proposed as a second non-literate-markdown specification_provider to carry that shape natively, the same way DMN is proposed for decision-table logic.

What already exists — confirmed by direct code audit (2026-08-19)

The specification_provider seam is real and already has two implementations

ComponentAuthoring.specification_provider: str (src/literate_ai/contracts/component_locking/authoring.py:378) is validated only as a non-empty string (string_value(...), no closed enum) — the contract layer is already open by design. Two providers exist today, both under src/literate_ai/adapters/specifications/:

SpecificationScenario mandates when/then at the contract level — this is load-bearing

src/literate_ai/contracts/specifications.py:51-94 — SpecificationScenario.__post_init__ (line 59) fail()s if when or then is empty. SpecificationSet (line 151) and SpecificationRequirement (line 97) both require at least one scenario / requirement. There is no per-provider variance point in this contract — every provider's output must resolve to one-or-more SpecificationRequirements each with one-or-more SpecificationScenarios, each with non-empty when/then. Both existing providers satisfy this by either literally authoring WHEN/THEN (OpenSpec) or synthesizing it (literate-markdown). An SCXML provider needs the same synthesis strategy — see the acceptance-oracle answer below.

Provider dispatch is a closed if/elif, not a registry — this is the actual provider-neutrality gap

Three call sites resolve specification_provider by string comparison, found by direct search (grep -rn "specification_provider ==" src/literate_ai/):

  1. _specification_references() (src/literate_ai/adapters/component_lock_planning.py:1573-1610) — if authoring.specification_provider == "openspec": ... elif == "literate-markdown": ... else: raise ComponentLockPlanningError("component_lock.specification_provider_unsupported", ...). This is the litai lock path.
  2. src/literate_ai/adapters/legacy_generation_catalog.py:601-613 — the same shape, else: raise ..."Component specification_provider must be openspec or literate-markdown". This is a litai generate-path call site.
  3. src/literate_ai/self_hosting.py:842 — if authoring.specification_provider != "literate-markdown": — this one is a deliberate narrower restriction (literate-ai's own self-hosted authoring is pinned to literate-markdown only) and should stay that way; it is not a gap to close.

Both real providers already share the same duck-typed shape by convention (not a formal Protocol): .load(root, paths, **kwargs) returning an object with .specification_set: SpecificationSet and .require_unchanged(root: Path) -> None. generation_preparation.py:434 only passes specification_provider through — it does not dispatch on it.

Generation-key binding already operates on raw artifact bytes, not parsed semantics

_specification_references() builds a ContentReference per declared specification_roots URI as a raw SHA-256 of file bytes (_reference(...)), then separately validates that the provider's parsed specification_set.artifacts identities match those same raw hashes (component_lock_planning.py:1603-1609, component_lock.specification_changed on mismatch). The generation key is bound to exact artifact bytes, uniformly across providers — it does not depend on what the bytes mean. This is true today for both OpenSpec Markdown and literate-Markdown, and needs no change to also be true for an SCXML XML document.

spec derive/spec review/spec accept/spec coverage are a different, WHEN/THEN-shaped pipeline

This is a load-bearing distinction the open questions' phrasing risks blurring, so it is worth stating precisely. litai spec derive|review|accept|coverage (src/literate_ai/cli/source_to_specification.py, backed by src/literate_ai/source_to_specification/contracts.py) is a reverse pipeline: it derives a specification from existing source code (DraftStatement/DraftScenario, BehaviorObservation/BehaviorSurface/CoverageState), not a forward-authored input to litai lock/litai generate. Its core scenario type is hardwired, not provider-neutral: DraftScenario (source_to_specification/contracts.py:450-458) has plain when: str / then: str fields with no provider dimension at all — there is no specification_provider concept anywhere in this pipeline's contracts. accept (cli/source_to_specification.py:2731) renders an accepted draft into either OpenSpec Markdown (synthesis.py:render_openspec_markdown/render_component_openspec_markdown) or literate-Markdown artifacts (synthesis.py:render_literate_markdown_artifacts) — the same two providers again, as targets this reverse pipeline writes into, not as providers this pipeline consumes generically. spec coverage/spec review as they exist today have no path for consuming a hand-authored SCXML document at all — they operate on source-derived WHEN/THEN drafts, and a hand-authored SCXML chart is a forward-authored specification input, structurally on the other side of this pipeline. See the direct answer to this open question below.

Grounding in the SCXML standard itself

SCXML (W3C State Chart XML: State Machine Notation for Control Abstraction) documents are well-formed XML with a root <scxml> element (namespace http://www.w3.org/2005/07/scxml, version="1.0", initial="<state-id>") containing:

Real SCXML tooling (Apache Commons SCXML, SCION, the W3C's own reference test suite) treats a chart as a single, self-contained document — there is no standard multi-file <xi:include>-equivalent in the base spec (some engines add one as an extension); this matters for the authoring-shape answer below.

Open questions — answered

1. Authoring/discovery shape for an SCXML document as a litai spec source

Answer: ComponentAuthoring.specification_provider = "scxml", specification_roots = ("spec/<name>.scxml",) — a single, complete, well-formed SCXML document per Component, mirroring how OpenSpec/literate-markdown roots are declared today. Concretely:

2. Acceptance-oracle shape for a state machine

The open question names three candidates: reachability/coverage of states and transitions, conformance to declared scenario traces, or something else. Answer: both of the first two, as two independent, complementary oracles — not a single either/or — because they check different things and only one of them is genuinely SCXML-specific.

3. Minimum viable adapter — parser, not interpreter

Answer: litai needs an SCXML parser and static-structure analyzer, not an SCXML interpreter. Generation is keyed off the static chart structure — the declared states, transitions, guard expressions (cond), and executable content (onentry/onexit actions) are extracted as data and handed to generation the same way DMN's table rows or OpenSpec's WHEN/THEN clauses are handed to generation today — with actual runtime execution, <datamodel> expression evaluation, the SCXML event-queue algorithm, and <send>/<invoke> external communication left entirely to the generated code, using whatever idiomatic state-machine pattern or library the target language's Flavor prescribes. This is explicitly the "structured-asset treatment, not a live spec engine" the roadmap issue anticipated, and it parallels assets:'s existing treatment of literal reference data (MEDIUM(a)) — the SCXML document is consumed as declarative structure, the same category of input assets: already treats non-prose reference data as. It also mirrors OpenSpecProvider's own explicit non-claim ("does not claim to replace the OpenSpec provider's own strict CLI validation") — SCXMLProvider should likewise not claim to be (or need to become) a W3C SCXML conformance-test-suite-grade interpreter. Building a full interpreter would mean reproducing genuinely hard runtime semantics (the SCXML processor algorithm, expression-language sandboxing, the event I/O processor) that litai has no product need for, since the actual execution happens in generated target-language code, not inside litai itself.

4. Generation-key binding, and spec coverage/spec review treatment

Generation-key binding: no change needed, same answer as DMN needs. As established above, _specification_references()'s content-hash mechanism operates uniformly on raw artifact bytes regardless of what those bytes mean — an SCXML .scxml file's SHA-256 becomes part of a Component's generation key exactly the way an OpenSpec .md file's hash does today, with zero new code at the identity/hashing layer. This is a direct consequence of the seam's existing design, not something either MEDIUM(b) or MEDIUM(c) needs to add.

spec coverage/spec review treatment: these commands, as they exist today, do not apply to a hand-authored SCXML document at all, and extending them is the wrong move — same conclusion DMN needs, reasoned here from SCXML's own code paths. As shown above, litai spec coverage/litai spec review belong to the reverse, source-derivation pipeline (DraftScenario's hardwired when/then, BehaviorSurface/CoverageState) — they derive a spec from existing source, then optionally render it into OpenSpec or literate-Markdown. A hand-authored SCXML chart is the opposite direction: a forward-authored input consumed before generation, structurally unrelated to what this reverse pipeline's contracts model. Two paths were considered:

5. litai lock/litai generate provider-neutrality

Answer once, for SCXML specifically confirming the general shape: yes, a change is needed, and it is small and mechanical — the contract layer is already open; only the imperative dispatch is closed. As shown above, ComponentAuthoring.specification_provider is validated only as a non-empty string at the contract layer — no schema change is needed to add "scxml" as a value. The actual work is replacing the two closed if/elif chains (component_lock_planning.py:_specification_references, legacy_generation_catalog.py:601-613) with a small registry (dict[str, SpecificationProviderFactory] or equivalent) keyed by provider_kind string, mapping to a provider conforming to the shape both existing providers already share by convention: .load(root, paths, **kwargs) returning .specification_set + .require_unchanged(root). Optionally formalize that duck-typed shape as a Protocol in application/ports.py (which already hosts other provider-shaped Protocols, e.g. the inspect(...) Protocol at line 16) so a third/fourth provider is checked structurally by the type system rather than only by convention. self_hosting.py:842's narrower literate-markdown-only restriction is deliberate project-bootstrap policy and should not be touched by this change. This is confirmed to be a small refactor (two call sites + one registry + one new provider module), not an architecture change — consistent with the roadmap document's framing that specification_provider is "an extension of an established extension point." This answer is identical for DMN — say so rather than re-deriving it per the task's own instruction: whichever of the two lands first should do this registry refactor once, and the second provider should land as a pure registry addition with no further dispatch-site changes.

Why TLA+/PlusCal is deliberately out of scope, and confirmation this design doesn't accidentally need it

TLA+/PlusCal's hard problem is verifying safety and liveness properties of concurrent, independently-scheduled processes under every possible interleaving — TLC model checking explores the combinatorial state space produced by multiple actors each progressing nondeterministically, to prove properties like mutual exclusion or eventual consistency hold under every schedule, not just the ones a developer anticipated. That is a fundamentally different — and harder — problem than validating one hierarchical/parallel state chart's own internal consistency.

Base SCXML, including its <parallel> construct, does not require solving that problem: <parallel> models concurrent regions within a single chart — all regions are active simultaneously and the parallel state completes when every region reaches a <final> — which is closed, structural, single-document semantics, not multiple independently-scheduled external processes whose relative ordering is unbounded. Every oracle proposed in this design is one of:

None of this reaches for a model checker, a temporal-logic property language, or interleaving exploration across multiple independently-scheduled processes — confirming this design does not accidentally take on TLA+'s harder problem to handle ordinary sequential (or single-chart-parallel) state machines. If a real Component's needs ever require proving properties across genuinely independent, concurrently-scheduled processes (e.g. a distributed consensus protocol, not a single workflow's state chart), that is precisely the narrower, not-yet-justified TLA+/PlusCal case 0.5.0-specification-hierarchy.md already reserves separately — nothing in this SCXML design should be stretched to cover it, and this design finds no evidence it needs to be.

Maturity / next-action assessment

Update (2026-08-19): the three follow-on steps below have now been prototyped. Artifacts live in docs/roadmap/0.6.0-scxml-prototype/:

Finding 1 (confirms the design, with one correction): reachability and transition-target resolution are mechanical, but only if the reachability walk treats <parallel> fan-out and ancestor-declared transitions correctly — a naive "per-state <transition> children only" graph undercounts real reachable behavior. SCXML transitions declared on a compound/parallel ancestor state are inherited by every descendant configuration (the spec's event-bubbling semantics) — in the prototype chart, power and standby are declared once on <state id="on"> and must be honored from every leaf underneath it (playing, paused, unmuted, muted, suspended), not just from on's immediate children. The original design's open question 2 described this as "pure graph reachability over the declared <state>/<parallel>/<final>/<history> graph," which is directionally right but undersells the work: a correct implementation must walk each active leaf's full ancestor chain to collect enabled transitions (Chart.enabled_transitions in the prototype), and must fan a <parallel> state's entry out into all regions' initial sub-states simultaneously when computing what configuration a transition leads to (Chart.entry). Both are still static, mechanical, no-interpreter-needed graph operations — the design's core claim holds — but "mechanical" undersold how much of SCXML's actual entry/exit algorithm a "just check reachability" implementation has to reproduce correctly to avoid false unreachable/dangling-target reports.

Finding 2 (an interaction the design didn't call out): the two structural checks are not independent — reachability must be resilient to dangling targets, not just report them separately. A first prototype pass crashed (KeyError) walking reachability through a transition whose target didn't resolve, because the reachability walker tried to compute the entry-configuration of a nonexistent state. The fix is simple (skip transitions with any unresolved target during the reachability walk; they are already reported by the target-resolution check) but this ordering/robustness requirement was not mentioned in the original design and would have produced a crash, not a clean diagnostic, in a first implementation attempt. Confirmed by deliberately introducing both a dangling transition target and an orphan unreachable state into a copy of the sample chart and re-running the checker: after the fix, both are reported as clean FAIL lines (not a traceback), and reverting the breakage restores a clean PASS.

Finding 3 (the declared-trace sidecar, now decided against the concrete sample): a separate file alongside the .scxml document, prototyped as JSON. Of the three placement options the design named:

Finding 4 (the one place the two oracles must NOT share an implementation): trace conformance requires real, stateful <history> tracking; structural reachability must NOT. The structural checker's Chart.entry() deliberately resolves a <history> pseudostate via its default transition only (there is no "last visited" state to fall back on when merely asking "can this state ever be reached at all") — that simplification is correct and sufficient for reachability/target-resolution, which only need a yes/no per state. Trace conformance is a different question — "does this specific run reach this exact configuration" — and requires a real interpreter that records each <history> node's last-active sub-configuration across steps and restores it on re-entry, not its default. The prototype's trace deliberately exercises this: power (off→on, no history yet) → pause → mute (now in {paused, muted}, inside the <parallel> region) → power (on→off, history must record {paused, muted}) → power (off→on again). The trace asserts the final power restores {paused, muted}, not the chart's default entry-configuration ({playing, unmuted}) — confirmed both ways: the real checker (apply_with_history, which records history before exiting) passes; a deliberately-history-blind variant of the same replay fails exactly that step with expected ['muted', 'paused'], got ['playing', 'unmuted'], proving the trace is actually exercising history state and not trivially satisfied by the simpler entry algorithm. Consequence for the provider design: SCXMLProvider's structural-review path and its trace-conformance path are not the same code walking two different inputs — the latter needs its own small stateful stepper, and that stepper (not the structural reachability walker) is the piece any future implementation should treat as the more delicate one to get right.

Shared bounded-snapshot/path-safety extraction (open question 3): still recommend deferring to whichever provider lands first, now slightly favoring DMN-or-shared timing. This prototype touched only parsing/graph logic, not the snapshot/path-safety layer at all — nothing here changes the original recommendation to extract _bounded_snapshot.py once, informed by both providers, rather than overfitting to one. Check the sibling DMN spike's own findings before deciding: if DMN's parsing prototype needed no format-placement decision as delicate as the trace-sidecar question above, DMN may be the simpler provider to land first and do the extraction as part of that first landing, with SCXML's SCXMLProvider (plus its now-decided .trace.json sidecar convention) arriving second as a pure registry addition per open question 5's answer.

Overall: closer to implementation-ready than the original spike, but not there yet. The trace-sidecar format is now concretely decided (separate JSON file, spec/<name>.trace.json) and validated end-to-end against a chart that actually has <parallel> and <history> in it, which was this design's one explicitly-named open piece. What remains before code, beyond ordinary implementation work: (a) porting the prototype's Chart/reachability/trace-replay logic from a throwaway ElementTree-based script into the real SCXMLProvider shape (bounded snapshot, SpecificationSet projection, the XXE-hardening decision the original design flagged and this prototype deliberately did not need to resolve, since it only ever parses a trusted local fixture), and (b) the still-open registry refactor (open question 5, shared with DMN) and the new litai spec scxml-review-shaped verb (open question 4) that would actually invoke these checks. Those are implementation tasks with a concrete shape now, not further open design questions.

Update (2026-08-20): the trace-sidecar format's own schema is now designed and prototyped, closing the "Next action" this document previously left open. The 2026-08-19 update above decided where the sidecar lives (a separate JSON file next to the .scxml document) and proved a stateful replay checker works end to end. It did not yet specify a reusable schema for that file. docs/history/roadmap/spikes/scxml-trace-prototype/RESULTS.md does exactly that: a small JSON schema ($schema, scxml, traces[].steps[] with event/expect_active/expect_regions/via_history/auto/note) validated against a second, independently-authored .scxml sample (connection_handshake.scxml, a connection-handshake protocol with two <parallel> regions and a deep <history>, deliberately a different domain from media_player.scxml so the format is shown to generalize rather than fit one fixture) and three prototyped trace documents (straight-line, parallel-region-independence, history-re-entry). A standalone trace_sidecar_validator.py proves the schema supports a cheap static structural check — every referenced state/region/history id resolves, every <parallel> configuration covers each region exactly once — as a fast first-pass complement to the sibling spike's stateful replay checker, confirmed to catch four distinct classes of malformed sidecar (unknown state id, incomplete parallel-region coverage, a via_history reference to a non-history node, an expect_regions entry inconsistent with chart structure) with specific errors rather than crashing or silently passing. Recommendation: this format is implementation-ready; no further design iteration was found necessary.

Summary table

Question Answer Confidence
Authoring/discovery shape Single .scxml file per Component via specification_provider = "scxml"; new SCXMLProvider mirroring OpenSpecProvider's bounded-snapshot shape High — direct precedent exists
Acceptance-oracle shape Two oracles: static structural soundness (reachability/transition-target resolution) + declared-trace conformance (separate .trace.json sidecar, prototyped) Structural: high, prototype-validated (with ancestor-inheritance and dangling-target-robustness corrections — see Maturity section). Trace format: decided and prototype-validated against a <parallel>+<history> sample; needs normal design review, not a further open question
Minimum viable adapter Parser + static analyzer, no interpreter; execution stays in generated code High — mirrors assets: treatment and OpenSpec's own non-claim
Generation-key binding No change needed; already byte-hash-based and provider-agnostic High — same answer DMN needs
spec coverage/spec review treatment Today's commands don't apply (reverse WHEN/THEN pipeline); needs its own SCXML-specific review verb High — same answer DMN needs
litai lock/litai generate provider-neutrality Contract already open; replace two if/elif dispatch sites with a registry, once, for all future providers High — same answer DMN needs
TLA+/PlusCal scope Confirmed not needed; every oracle here is static-graph or delegated-to-generated-code, never interleaving/model-checking High
Overall maturity Prototype-validated; trace-sidecar format decided (separate .trace.json); remaining work is ordinary implementation (provider module, registry refactor, review verb), not further open design questions —
Read the Markdown sourceConference homePublished 1.3.0 · Patch 1.3.1 in progress · Development 1.4