XTAL (intent → spec)

XTAL provides a spec-first surface for X07 projects:

• *.x07spec.json modules are the canonical intent/behavior interface.
• Optional *.x07spec.examples.jsonl example cases provide a minimum semantic oracle.
• A deterministic generator converts examples and declared properties into normal X07 tests under gen/xtal/.

Example projects:

• Smallest end-to-end: docs/examples/agent-gate/xtal/toy-sorter/
• Branded multi-operation library surface: docs/examples/agent-gate/xtal/workflow-graph/
• Complex app slices: start from a passing app test baseline, then expose a narrow pure helper surface under XTAL instead of targeting the full CLI, reducer, OS, or replay entrypoint.

Artifacts

XTAL manifest (x07.xtal.manifest@0.1.0)

• Location: arch/xtal/xtal.json
• Schema: x07.xtal.manifest@0.1.0 (see docs/spec/schemas/x07.xtal.manifest@0.1.0.schema.json)
• Provides:
  • entrypoints[] for certification targets
  • trust.cert_profile and trust.review_gates[] for certification review gates
  • autonomy.agent_write_paths[] and autonomy.agent_write_specs|agent_write_arch for repair boundaries
• See also: docs/toolchain/xtal-targets.md.

Spec modules (x07.x07spec@0.1.0)

• Location: spec/<module_id>.x07spec.json (recommended)
• Schema: x07.x07spec@0.1.0 (see docs/spec/schemas/x07.x07spec@0.1.0.schema.json)

Example cases (x07.x07spec_examples@0.1.0, JSONL)

• Location: spec/<module_id>.x07spec.examples.jsonl (optional)
• Schema: x07.x07spec_examples@0.1.0 (see docs/spec/schemas/x07.x07spec_examples@0.1.0.schema.json)
• One JSON object per line.

Minimum value encodings:

• bytes / bytes_view: {"kind":"bytes_b64","b64":"..."}
• i32: a JSON integer (and the object form {"kind":"i32","i32":123} / {"kind":"i32","value":123} is accepted)

Properties (ensures_props)

Each operation can declare ensures_props[] entries that reference a property function.

• The property function is executed under property-based testing (PBT).
• The property function MUST return a bytes_status_v1 payload (see std.test.status_ok / std.test.status_fail).
• ensures_props[*].args[] selects which operation parameters are passed to the property function.
• x07 xtal impl check enforces that the referenced function exists, is exported, has a compatible signature for the selected args (including brands), and returns bytes.

Branded bytes (canonical example)

If you use brands on public byte boundaries, keep the brand ids aligned across:

• spec/*.x07spec.json: operations[*].params[*].brand and operations[*].result_brand
• src/*.x07.json: defn.params[*].brand and defn.result_brand
• generated property wrappers: gen/xtal/**/tests.x07.json (generated from spec)
• boundary index: arch/boundaries/index.x07boundary.json

Concrete reference: docs/examples/agent-gate/xtal/workflow-graph/.

Key files:

• Spec brands: docs/examples/agent-gate/xtal/workflow-graph/spec/workflow.graph.x07spec.json
• Impl brands: docs/examples/agent-gate/xtal/workflow-graph/src/workflow/graph.x07.json
• Generated wrappers: docs/examples/agent-gate/xtal/workflow-graph/gen/xtal/workflow/graph/tests.x07.json
• Boundary brands: docs/examples/agent-gate/xtal/workflow-graph/arch/boundaries/index.x07boundary.json

Commands

Authoring

• x07 xtal spec scaffold --module-id <id> --op <local_name> --param <name:ty> --result <ty> [--examples] [--out-path <path>]
• x07 xtal spec fmt --input <spec.x07spec.json> --write [--inject-ids]
• x07 xtal spec extract --project x07.json (--module-id <id> | --impl-path <path>) (--write | --patchset-out <path>)

For deterministic multi-file edits that touch JSON specs, implementation modules, and manifests, prefer an x07.patchset@0.1.0 plus:

• x07 patch apply --in <patchset.json> --repo-root . --write

x07 patch apply currently applies RFC 6902 patches to JSON documents. Edit *.examples.jsonl streams directly, then regenerate tests so their digests are recorded in the XTAL report.

Then run x07 fmt on changed x07AST files, x07 xtal spec fmt on changed *.x07spec.json files, and x07 xtal tests gen-from-spec --write. Do not edit gen/xtal/** directly.

Validation

• x07 xtal spec lint --input <spec.x07spec.json>
• x07 xtal spec check --project x07.json --input <spec.x07spec.json>
  • Validates op ids, signatures, contract clause type/purity checks, and example cases.

Tests generation (examples → unit tests)

• x07 xtal tests gen-from-spec --project x07.json --write
  • Writes:
    • gen/xtal/tests.json (x07.tests_manifest@0.2.0)
    • gen/xtal/<module_path>/tests.x07.json (module_id: gen.xtal.<module_id>.tests)
  • Generates:
    • unit tests from examples (returns result_i32)
    • PBT property wrappers for ensures_props (returns bytes_status_v1)
• x07 xtal tests gen-from-spec --project x07.json --check
  • Fails if any generated output would change (drift check).

Run generated tests with the same selection rules as any other X07 manifest:

• x07 test --manifest gen/xtal/tests.json runs the non-PBT example tests.
• x07 test --pbt --manifest gen/xtal/tests.json runs the generated property tests.
• x07 test --all --no-fail-fast --manifest gen/xtal/tests.json runs examples and properties in one lane.
  • Use the --all form for manual XTAL validation when specs declare ensures_props; otherwise the generated property wrappers are not selected.

Implementation conformance

• x07 xtal impl check --project x07.json
  • Validates that each spec module has a corresponding implementation module under src/.
  • Validates exports, signatures, and contract-core clause alignment.
• x07 xtal impl sync --project x07.json --write
  • Creates missing modules and stubs, adds missing exports, and syncs contract-core clauses.
  • If --patchset-out <path> is provided, emits an x07.patchset@0.1.0 instead of writing files.
  • Requires deterministic clause ids for contract-core clauses (use x07 xtal spec fmt --inject-ids --write).

End-to-end wrapper

• x07 xtal dev
  • Runs spec fmt/lint/check.
  • If arch/gen/index.x07gen.json exists (or --gen-index is passed), runs x07 gen verify.
  • Otherwise, runs x07 xtal tests gen-from-spec --check.
  • Runs x07 xtal impl check.
  • Unless --prechecks-only is set, runs x07 xtal verify.
  • Forwards proof/verification controls to the verification step: --entry, --test-filter, --test-exact, --proof-policy, --allow-os-world, --unwind, --max-bytes-len, --input-len-bytes, --z3-timeout-seconds, and --z3-memory-mb.
  • If verification fails and --repair-on-fail is set, runs x07 xtal repair --write.
  • The JSON report includes meta.summary, a compact agent-facing view of precheck status plus the forwarded verification settings and results when verification ran.
• x07 xtal verify
  • Runs spec/gen/impl prechecks.
  • Requires a deterministic solve-* world by default (pass --allow-os-world to override).
  • Runs formal verification per spec operation entrypoint:
    • x07 verify --coverage --entry <spec.operations[*].name>
    • x07 verify --prove --entry <spec.operations[*].name> --emit-proof <path>
  • --entry <name-or-id> can be passed more than once to restrict the coverage/proof lane to matching spec operation names or ids.
    • Use the full spec operation name or id, for example --entry op.app.foo.bar_v1.v1; generated test id substrings belong under --test-filter.
  • Runs x07 test --all --no-fail-fast --manifest gen/xtal/tests.json --allow-empty.
    • By default this keeps the generated tests as a full regression gate.
    • Pass --test-filter <substr> to forward x07 test --filter <substr> for focused generated-test runs; add --test-exact to require an exact generated test id match.
  • Writes:
    • target/xtal/xtal.verify.diag.json (wrapper diagnostics report, x07diag.report@0.3.0)
    • target/xtal/verify/summary.json (aggregate summary, x07.xtal.verify_summary@0.1.0; see docs/spec/schemas/x07.xtal.verify_summary@0.1.0.schema.json)
    • target/xtal/tests.report.json (test report)
    • target/xtal/verify/_artifacts/ (nested artifacts for x07 verify and x07 test)
      • target/xtal/verify/_artifacts/verify/... (proof counterexamples, solver inputs, CBMC/Z3 intermediates)
      • target/xtal/verify/_artifacts/test/... (property-test repro cases and other test artifacts)
    • target/xtal/verify/coverage/<module_path>/<local>.report.json (per-entry coverage reports)
    • target/xtal/verify/prove/<module_path>/<local>.report.json (per-entry prove reports)
    • target/xtal/verify/prove/<module_path>/<local>/proof.object.json (proof objects, when emitted)
  • Paths in the XTAL JSON report are project-root-relative. If you invoke x07 xtal verify --project subdir/x07.json from a parent directory, look under subdir/target/xtal/....
  • target/xtal/verify/summary.json records the effective settings.entry_filter, settings.test_filter, settings.verify_bounds, and settings.proof_budget values used for the proof and test lanes.
  • Proof outcomes are controlled by --proof-policy {balanced|strict} (default: balanced).
    • Under balanced, missing proof tools produce warnings (and verification continues).
    • Under strict, only proven outcomes pass.
  • When proofs are unsupported or inconclusive, the wrapper emits a compact per-entry reason summary in the XTAL diagnostics (for example: unsupported loop forms or unsupported branded input shapes).
  • Always inspect target/xtal/verify/summary.json after a warning. The top-level ok: true can coexist with per-entry prove.policy_outcome: "warn" under balanced; use the per-entry prove.raw value and optional prove.first_diagnostic code/message to decide whether the operation actually has proof evidence.
  • Keep proof-facing modules inside the certifiable pure subset. Native-handle helpers whose implementations depend on internal-only builtins, such as std.hash_map.emit_kv_u32le_u32le via map_u32.dump_kv_u32le_u32le, can make affected entries report prove.raw: "unsupported" even when generated tests and coverage pass. Prefer byte-encoded pure structures such as std.btree_map for proof-facing paths, or isolate native-handle helpers behind dedicated entries and confirm the impact in target/xtal/verify/summary.json.
  • When adapting a larger example or app, preserve the manifest dependencies and keep x07.lock.json aligned with the scratch manifest. A module can look local and pure while still importing package-provided helpers such as std.crawl.* or std.web_ui.*; removing those dependencies can make generated tests or verification fail with lockfile/module-root diagnostics instead of measuring the intended XTAL surface.
  • If coverage and generated tests pass but proof reports X07V_PROOF_SUMMARY_REQUIRED, the operation reached an imported helper that has no loaded proof summary. Treat that as a proof-surface boundary: either target a smaller local helper, add/import the required proof summary, or record the entry as test/coverage-validated but not proof-proven.
  • For full-stack API examples that call broad stdlib parsers such as std.json.extract_path_canon_or_err, run coverage first and inspect uncovered_defn, recursive_defn, and the per-function details fields before starting a broad proof lane. A small local adapter can look supported while the reachable closure contains many no-contract std.json/std.vec helpers; generated tests may still be the right evidence until those helpers have proof summaries or the adapter is narrowed.
  • For web-ui reducers and other large state machines, expose small deterministic helpers for JSON/path/key/string transformations first. Adding contracts directly to broad reducer helpers can widen the verification obligation for unrelated reducer paths; a dedicated proof-facing adapter is usually easier to reason about.
  • Verification bounds can be overridden with --unwind, --max-bytes-len, and --input-len-bytes.
  • Under --proof-policy balanced, xtal verify uses conservative proof budgets so the default loop stays bounded.
    • Defaults: --unwind 1, --max-bytes-len 8, --z3-timeout-seconds 1.
  • The Z3 timeout for the proof lane can be overridden with --z3-timeout-seconds (otherwise x07's default timeout applies under --proof-policy strict).
  • --z3-timeout-seconds bounds the Z3 solver call, not CBMC/SMT2 generation. If a std.json-heavy or std.vec-heavy proof entry produces coverage artifacts but no prove report, rerun a focused entry with an external process timeout and treat the missing prove report as verifier setup cost rather than a solver result.
  • The Z3 solver memory limit can be set with --z3-memory-mb.
  • Treat X07V_SMT_TIMEOUT as a proof-design signal, not just a request for a larger timeout. Nested data-dependent scans, repeated calls into scanning helpers, and broad byte bounds can make the SMT obligation grow quickly; try a smaller proof-facing entrypoint, tighter byte/input bounds, or a helper with its own proof summary before raising solver budgets. Higher timeouts are useful for measurement, but can also increase peak memory substantially.
  • Small bytes.concat builders can also time out when the postcondition relates bytes.len(__result) to symbolic input lengths. For JSON or effects-array assembly helpers, keep exact byte output coverage in examples and start proof contracts with simple fixed-shape guarantees; add symbolic length relationships only after a focused --entry run proves they are affordable.
  • If an operation times out under balanced policy, the timeout diagnostic includes the effective proof budget. Compare that with settings.proof_budget.z3_timeout_seconds and a targeted x07 verify --prove --entry ... --z3-timeout-seconds <n> run before changing the implementation.
  • A narrower spec operation only reduces proof cost when the implementation body is narrower too. If it still calls an unproved generic scanner inside its loop, the summary can keep reporting prove.raw: "timeout" for the new operation.
  • When a proof-facing operation composes helpers that accept owned bytes, bind public byte params as views before the loop and pass view.to_bytes(<view>) copies into the helper. Passing the original param directly can move it and make generated wrappers fail with use after move when postconditions or later expressions still reference it.
  • Proof caching is automatic when a project manifest is available:
    • Successful x07 verify --prove runs cache proof summaries under .x07/cache/verify/proof_summaries/.
    • When proof objects are emitted, proof bundles are cached under .x07/cache/verify/proofs/ and may be reused on subsequent prove runs (even without solver tools present).
  • Proof runs require external tooling; see docs/toolchain/formal-verification.md.
• x07 xtal certify
  • Requires arch/xtal/xtal.json.
  • Optionally runs x07 xtal dev prechecks (skip with --no-prechecks).
  • Uses --spec-dir <dir> (default: spec) to bind spec/example inputs into the certification bundle manifest.
  • Selects entrypoints from the XTAL manifest (pass --entry to pick one, or --all to certify all).
  • For each entrypoint, runs x07 trust certify with:
    • --profile <trust.cert_profile>
    • --baseline <path> (optional, enables review diff outputs)
    • --review-fail-on <gate> for each trust.review_gates[] entry
    • --no-fail-fast (optional; preserve full test signal after the first failure)
    • Proof budgets forwarded to x07 verify --prove: --unwind, --max-bytes-len, --input-len-bytes, --z3-timeout-seconds, --z3-memory-mb
  • Writes:
    • target/xtal/xtal.certify.diag.json (wrapper diagnostics report, x07diag.report@0.3.0)
    • target/xtal/cert/summary.json (x07.xtal.certify_summary@0.1.0; see docs/spec/schemas/x07.xtal.certify_summary@0.1.0.schema.json)
    • target/xtal/cert/bundle.json (x07.xtal.cert_bundle@0.1.0; digests for the certification outputs plus bound spec/example inputs)
    • target/xtal/cert/<entry>/... (certificate bundles and trust artifacts from x07 trust certify)
• x07 xtal repair
  • Reads target/xtal/verify/summary.json (baseline) and attempts a bounded repair for one failing entry.
  • Strategies:
    • semantic attempt for prove.raw == "counterexample" entries (enumerative single-expression synthesis for i32 results, pruned by spec examples and validated by targeted x07 test then x07 verify --prove)
    • quickfix fallback via x07 fix when semantic repair is unavailable or fails
  • If --write is set, requires arch/xtal/xtal.json, enforces autonomy.agent_write_paths[] for patch targets, applies the final patchset to the working tree, and reruns x07 xtal verify.
  • By default, only edits known stub bodies (pass --allow-edit-non-stubs to override).
  • Flags: --write, --max-rounds, --max-candidates, --semantic-max-depth, --semantic-ops, --entry, --stubs-only, --semantic-only, --quickfix-only, --suggest-spec-patch.
  • Writes:
    • target/xtal/xtal.repair.diag.json (wrapper diagnostics report, x07diag.report@0.3.0)
    • target/xtal/repair/summary.json (x07.xtal.repair_summary@0.1.0; see docs/spec/schemas/x07.xtal.repair_summary@0.1.0.schema.json)
    • target/xtal/repair/patchset.json (x07.patchset@0.1.0)
    • target/xtal/repair/diff.txt (deterministic review diff)
    • target/xtal/repair/attempts/attempt-0001/... (per-attempt evaluation artifacts)

Output conventions

• Generated test module id: gen.xtal.<module_id>.tests
• Generated unit test entrypoints: gen.xtal.<module_id>.tests.ex_0001, ...ex_0002, …
• Generated property wrapper entrypoints: gen.xtal.<module_id>.tests.prop_0001, ...prop_0002, …
• Manifest unit test ids: xtal/<module_id>/<op_id>/ex0001, .../ex0002, …
• Manifest property test ids: xtal/<module_id>/<op_id>/prop0001, .../prop0002, …
• XTAL reports record deterministic input digests in meta.spec_digests and meta.examples_digests (sha256 + bytes_len) for review/trust artifacts.

Runtime violations

When a runtime contract violation is detected (for example via x07 test or x07 run), x07 can write a self-contained violation bundle under target/xtal/violations/<id>/.

By default, this is enabled when the project has arch/xtal/xtal.json. To override the output directory (or to enable it for non-XTAL projects), set X07_XTAL_VIOLATIONS_DIR (absolute, or relative to the project root).

Artifacts:

• target/xtal/violations/<id>/violation.json (x07.xtal.violation@0.1.0)
• target/xtal/violations/<id>/repro.json (x07.contract.repro@0.1.0)

OS-world incidents: when a contract violation is captured from run-os or run-os-sandboxed, x07 run rewrites the emitted repro to world: "solve-rr" and captures .x07_rr/ into .x07/artifacts/contract/<clause_id>/rr/ (referenced via runner.fixture_rr_dir).

See: docs/worlds/record-replay.md.

Recovery events

When a runtime violation is recorded, x07 can also emit a structured recovery event stream (JSONL).

By default, this is enabled when the project has arch/xtal/xtal.json. To override the output directory (or to enable it for non-XTAL projects), set X07_XTAL_EVENTS_DIR (absolute, or relative to the project root).

Artifacts:

• target/xtal/events/<id>/events.jsonl (JSONL; each line is x07.xtal.recovery_event@0.1.0)

See: Task policy graph.

x07 xtal ingest

Normalize a violation (x07.xtal.violation@0.1.0) or a contract repro (x07.contract.repro@0.1.0) into a canonical ingest workspace (and, by default, run an improvement loop).

Ingest validates that violation.json matches repro.json (content-addressed id, repro sha256, and repro bytes length), and records the check results in the ingest summary.

By default, ingest also runs x07 xtal improve on the normalized workspace. To stop after normalization, pass --normalize-only.

Artifacts:

• target/xtal/xtal.ingest.diag.json (x07diag.report@0.3.0)
• target/xtal/ingest/summary.json (x07.xtal.ingest_summary@0.1.0)
• target/xtal/ingest/<id>/violation.json (x07.xtal.violation@0.1.0)
• target/xtal/ingest/<id>/repro.json (x07.contract.repro@0.1.0)
• target/xtal/ingest/<id>/events.jsonl (optional; copied when ingesting events.jsonl)

x07 xtal improve

Turn incident inputs (violation bundles, contract repros, or recovery event logs) into a bounded improvement run:

• x07 xtal improve --input <path>
• Optional: --reduce-repro, --write, --allow-spec-change, --certify, --run-tasks, --baseline <cert_dir>, --out-dir <dir>

Artifacts:

• target/xtal/xtal.improve.diag.json (x07diag.report@0.3.0)
• target/xtal/improve/summary.json (x07.xtal.improve_summary@0.1.0)
• target/xtal/improve/<id>/tests.shadow.json (generated single-case tests manifest)
• target/xtal/improve/<id>/repro.min.json and target/xtal/improve/<id>/reduction.report.json (optional; when --reduce-repro is supported)

x07 xtal tasks run

Execute recovery tasks from arch/tasks/index.x07tasks.json for an incident input:

• x07 xtal tasks run --input target/xtal/violations/<id>/violation.json

Artifacts:

• target/xtal/xtal.tasks.diag.json (x07diag.report@0.3.0)
• target/xtal/tasks/<id>/... (generated wrappers + per-attempt stderr captures)
• target/xtal/events/<id>/events.jsonl (optional; when recovery events are enabled)

Execution conventions:

• Each task must reference a defn/defasync symbol that returns bytes.
• Supported task parameter shapes:
  • 0 params
  • 1 param: bytes_view (receives the built-in input) or bytes (receives view.to_bytes(input)).