Building an X07 Service: From Scaffold to Certificate
Previously: How to Trust X07 Code Written by Coding Agents
The previous posts explained why X07 exists and how its trust model works. This post walks through doing it — scaffolding a service, adding domain logic, wiring tests and contracts, and producing the kind of certificate bundle that lets a reviewer approve a change without reading the whole source tree.
Everything below is something a coding agent can execute in one session. That is the point.
Step 1: Scaffold the service
X07 ships service templates that produce a working project in one command. The five built-in archetypes are api-cell, event-consumer, scheduled-job, policy-service, and workflow-service. Each maps to a specific ingress kind, runtime class, and scale class.
For this walkthrough we will use api-cell — an HTTP service backed by Postgres and S3-compatible object storage.
# Scaffold a new project from the api-cell service archetype.
mkdir orders
cd orders
x07 init --template api-cell
As of x07 0.1.102, service archetype scaffolds (api-cell, event-consumer, etc) are not yet usable from the prebuilt x07 binary alone. If x07 init --template api-cell fails, run it via a source checkout:
cargo run -q -p x07 --manifest-path /path/to/x07/Cargo.toml -- init --template api-cell
That single command produces a complete, buildable project:
orders/
x07.json # project manifest
x07.lock.json # pinned dependency graph
x07-toolchain.toml # toolchain channel + offline docs
AGENT.md # self-recovery guide for agents
README.md # scaffold README
.agent/ # offline docs + skills (symlinked)
.x07/ # resolved dependency checkout (from x07.lock.json)
src/
main.x07.json # program entry (wires to the domain)
example.x07.json # starter domain module
arch/
manifest.x07arch.json # architecture rules
service/
index.x07service.json # service manifest (cells, topology, bindings)
policy/
run-os.json # sandbox policy for run-os-sandboxed
tests/
tests.json # test manifest
core.x07.json # starter smoke test module
The project already runs:
# Run the scaffolded service inside the default sandbox profile.
x07 run --profile sandbox
Nothing interesting happens yet — the starter domain module returns an empty byte buffer. The point is that every piece of infrastructure is already wired and the repair loop works from the first command.
Step 2: Understand the service manifest
The file arch/service/index.x07service.json is the architectural spine of the service. It declares what the service is without deciding how it gets deployed.
This JSON is part of the X07 service architecture system. Comments explain each field for readers new to X07.
{
"schema_version": "x07.service.manifest@0.1.0", // Service manifest format version.
"service_id": "orders", // Unique service identifier.
"display_name": "Orders", // Human-readable name.
"domain_pack": {
"id": "orders", // The authoring unit agents edit.
"display_name": "Orders"
},
"cells": [
{
"cell_key": "api", // Unique key for this operational cell.
"cell_kind": "api-cell", // Archetype: HTTP API service.
"entry_symbol": "orders.api.main", // The x07AST symbol that handles requests.
"ingress_kind": "http", // Traffic enters over HTTP.
"runtime_class": "native-http", // Compiled native binary with HTTP adapter.
"scale_class": "replicated-http", // Horizontally scaled behind a load balancer.
"binding_refs": ["db.primary", "obj.documents"], // Logical dependencies (not cloud products).
"topology_group": "primary" // Co-location hint for topology profiles.
}
],
"topology_profiles": [
{
"id": "dev",
"target_kind": "hosted", // Single deployable for local and hosted dev.
"placement": "co-located"
},
{
"id": "prod",
"target_kind": "k8s", // Kubernetes with independent cell scaling.
"placement": "split-by-cell"
}
],
"resource_bindings": [
{ "name": "db.primary", "kind": "postgres", "required": true }, // Logical Postgres binding.
{ "name": "obj.documents", "kind": "s3", "required": false } // Logical S3-compatible binding.
],
"default_trust_profile": "sandboxed_service_v1"
}
Three things to notice:
-
Cells are the unit of release and trust. Each cell has one entry symbol, one ingress kind, one runtime class, and one trust boundary. That is not accidental — it keeps the reviewable surface small.
-
Bindings are logical. The service code says
db.primary, notpostgres://prod-cluster-3.us-east-1.rds.amazonaws.com. Cloud-specific wiring happens at deploy time, outside the service repo. -
Topology is late. The same domain pack can run as one co-located binary in dev and split into independent Kubernetes deployments in prod. The agent does not need to know which.
# Validate the service manifest against the archetype schema.
x07 service validate --manifest arch/service/index.x07service.json
Step 3: Add pure domain logic
The most important code in an X07 service lives in the pure domain kernel. This is the part that can be formally verified, deterministically tested, and certified.
In practice, you typically certify the kernel as its own solve-pure project/package, and keep the service shell as a separate run-os-sandboxed service project that depends on it.
This example uses X07's canonical x07AST JSON format. The comments explain what each field means for readers who are new to the language.
{
"schema_version": "x07.x07ast@0.8.0", // x07AST format version.
"kind": "module", // This file defines an x07 module.
"module_id": "orders.core", // Fully qualified module name.
"imports": [], // No external dependencies — pure logic only.
"decls": [
{
"kind": "defn", // Define a pure, synchronous function.
"name": "orders.core.compute_total_v1", // Stable module-qualified symbol name.
"params": [
{ "name": "item_count", "ty": "i32" }, // Number of items in the order.
{ "name": "unit_price", "ty": "i32" }, // Price per item in cents.
{ "name": "discount_pct", "ty": "i32" } // Discount percentage (0-100).
],
"result": "i32", // Returns the total in cents.
"requires": [
{ "id": "valid_count", "expr": [">=", "item_count", 0] },
{ "id": "valid_price", "expr": [">=", "unit_price", 0] },
{ "id": "bound_discount", "expr": ["and",
[">=", "discount_pct", 0],
["<=", "discount_pct", 100]] }
],
"ensures": [
{ "id": "non_negative", "expr": [">=", "__result", 0] }
],
"body": ["begin",
["let", "subtotal", ["*", "item_count", "unit_price"]],
["let", "reduction", ["/", ["*", "subtotal", "discount_pct"], 100]],
["-", "subtotal", "reduction"]
]
},
{
"kind": "export", // Make the symbol visible to other modules.
"names": ["orders.core.compute_total_v1"]
}
]
}
A few things worth pointing out:
-
requiresandensuresare contracts, not comments. They are machine-checkable and the verifier uses them as proof obligations. Theidon each clause gives diagnostics and review artifacts a stable name to reference. -
The body is an expression tree, not text. An agent does not need to parse indentation or deal with syntax ambiguity. It edits a tree, and the toolchain validates the tree.
-
There are no imports. This function is pure — it depends on nothing outside its own parameters. That purity is what makes formal verification practical rather than aspirational.
Step 4: Pin the boundary
A pure function is not useful until something calls it. The boundary between the pure kernel and the outside world is where most bugs live — wrong field order, wrong encoding, silent format drift.
X07 pins that boundary explicitly:
# Generate validators, encoders, and deterministic tests from the API schema.
x07 schema derive \
--input arch/web/api/orders_v1.x07schema.json \
--out-dir gen \
--write
The boundary index pins the reviewable surface explicitly:
The boundary index is required by strong trust profiles, and is validated by both x07 arch check and x07 trust certify.
// arch/boundaries/index.x07boundary.json
{
"schema_version": "x07.arch.boundaries.index@0.1.0",
"boundaries": [
{
"id": "orders.core.compute_total_v1",
"symbol": "orders.core.compute_total_v1",
"node_id": "domain_core",
"kind": "public_function",
"from_zone": "verified_core",
"to_zone": "verified_core",
"worlds_allowed": ["solve-pure"],
"input": {
"params": [
{ "name": "item_count", "ty": "i32" },
{ "name": "unit_price", "ty": "i32" },
{ "name": "discount_pct", "ty": "i32" }
]
},
"output": { "ty": "i32" },
"smoke": {
"entry": "tests.core.smoke_compute_total",
"tests": ["smoke/compute_total"]
},
"pbt": {
"required": true,
"tests": ["pbt/total_non_negative"]
},
"verify": {
"required": true,
"mode": "prove"
}
}
]
}
And the architecture manifest declares which modules belong to which trust zones:
{
"schema_version": "x07.arch.manifest@0.3.0",
"repo": { "id": "orders", "root": "." },
"externals": {
"allowed_import_prefixes": ["std."], // Only standard library imports allowed.
"allowed_exact": ["std.test"]
},
"nodes": [
{
"id": "domain_core", // The pure domain kernel.
"match": {
"module_prefixes": ["orders.core"],
"path_globs": ["src/orders/core/**/*.x07.json"]
},
"world": "solve-pure", // Must run in the deterministic pure world.
"trust_zone": "verified_core", // Eligible for formal verification.
"visibility": {
"mode": "restricted",
"visible_to": ["service_shell", "tests"]
},
"imports": {
"deny_prefixes": ["std.os.", "ext."], // No OS or external imports allowed.
"allow_prefixes": ["orders.core", "std."]
}
},
{
"id": "service_shell", // The effectful adapter layer.
"match": {
"module_prefixes": ["orders.api"],
"path_globs": ["src/orders/api/**/*.x07.json"]
},
"world": "run-os-sandboxed", // Runs with real OS access under sandbox policy.
"trust_zone": "untrusted", // Reviewed via capsule attestation, not proof.
"visibility": { "mode": "public", "visible_to": [] },
"imports": {
"deny_prefixes": [],
"allow_prefixes": ["orders.", "std.", "ext."]
}
},
{
"id": "tests",
"match": {
"module_prefixes": ["tests."],
"path_globs": ["tests/**/*.x07.json"]
},
"world": "solve-pure",
"trust_zone": "test_only",
"visibility": { "mode": "restricted", "visible_to": [] },
"imports": {
"deny_prefixes": [],
"allow_prefixes": ["orders.", "std.", "tests."]
}
}
],
"rules": [
{ "kind": "layers_v1", "id": "layers.v1",
"layers": ["domain_core", "service_shell", "tests"],
"direction": "down" }, // Tests can import service_shell, not the reverse.
{ "kind": "deny_cycles_v1", "id": "no_cycles", "scope": "nodes" }
],
"contracts_v1": {
"boundaries": {
"index_path": "arch/boundaries/index.x07boundary.json",
"enforce": "error"
},
"canonical_json": { "mode": "jcs_rfc8785_v1" }
},
"checks": {
"deny_cycles": true,
"deny_orphans": true,
"enforce_visibility": true,
"enforce_world_caps": true,
"brand_boundary_v1": { "enabled": true },
"allowlist_mode": {
"enabled": true,
"default_allow_external": false,
"default_allow_internal": false
}
},
"tool_budgets": {
"max_modules": 5000,
"max_edges": 50000,
"max_diags": 2000
}
}
# Validate the architecture rules. Fix any violations deterministically.
x07 arch check --write
This is where X07 catches the kind of mistake that an agent makes most often: importing the wrong layer, smuggling effects into the core, or widening capability posture without making it obvious. The architecture manifest turns those implicit rules into data the toolchain can enforce.
Step 5: The agent repair loop
The normal development loop in X07 is: edit, run, watch the repair cycle.
# Run the project with auto-repair enabled (the default).
# The toolchain will format, lint, apply quickfixes, and retry automatically.
x07 run
Under the hood, x07 run does this:
Every diagnostic is structured JSON, not a paragraph of prose. Every quickfix is a JSON Patch the agent can apply mechanically. The loop converges or produces a clear error an agent can parse — there is no "guess what the compiler meant" step.
When the repair loop is not the right tool (for example, when debugging a logic error), turn it off:
# Run without auto-repair — see raw diagnostics instead.
x07 run --repair=off
Step 6: Tests — smoke and property-based
X07 keeps all test configuration in one manifest:
This test manifest uses the X07 testing system. Comments explain each field.
{
"schema_version": "x07.tests_manifest@0.2.0",
"tests": [
{
"id": "smoke/compute_total", // Human-readable test identifier.
"entry": "tests.core.smoke_compute_total", // The x07AST symbol that runs this test.
"expect": "pass", // Expected outcome.
"world": "solve-pure" // Run deterministically — no OS, no randomness.
},
{
"id": "pbt/total_non_negative", // Property-based test identifier.
"entry": "tests.core.pbt_total_non_negative",
"expect": "pass",
"world": "solve-pure",
"returns": "bytes_status_v1", // PBT functions return a structured status byte.
"pbt": {
"cases": 64, // Generate 64 random test cases.
"max_shrinks": 32, // Shrink counterexamples up to 32 times.
"params": [
{ "name": "item_count", "gen": { "kind": "i32", "min": 0, "max": 1000 } },
{ "name": "unit_price", "gen": { "kind": "i32", "min": 0, "max": 100000 } },
{ "name": "discount_pct", "gen": { "kind": "i32", "min": 0, "max": 100 } }
],
"case_budget": {
"fuel": 100000, // Max computation steps per case.
"timeout_ms": 250, // Wall-clock timeout per case.
"max_mem_bytes": 16777216 // 16 MB memory cap per case.
}
}
}
]
}
# Run all tests — both smoke and PBT.
x07 test --all --manifest tests/tests.json
The PBT test generates random inputs within the declared ranges, runs the function, checks the contract postconditions, and if anything fails, shrinks to the smallest counterexample. That gives a reviewer a much better question than "did the tests pass?" — the question becomes: did this function survive 64 generated cases across the full input space and produce a stable, minimal counterexample when it failed?
If PBT finds a counterexample:
# Replay the exact failing case for debugging.
x07 test --pbt --pbt-repro target/x07test/pbt/id_<sha256(test-id)>/repro.json \
--manifest tests/tests.json
# Convert the repro into a deterministic regression test and patch the manifest.
x07 fix --from-pbt target/x07test/pbt/id_<sha256(test-id)>/repro.json \
--tests-manifest tests/tests.json \
--write
Step 7: Formal verification
Tests show that the function works on the cases you tried. Formal verification shows that the contracts hold for all inputs.
# Check what the verifier can reason about for this entry symbol.
x07 verify --coverage --entry orders.core.compute_total_v1
# Generate proof evidence.
x07 verify --prove \
--entry orders.core.compute_total_v1 \
--emit-proof target/prove/compute_total.proof.json
# Independently check the proof artifact.
x07 prove check --proof target/prove/compute_total.proof.json
Three commands, three distinct things:
-
Coverage tells you what the verifier can support — which symbols are reachable, which have contracts, and which fall outside the certifiable subset.
-
Prove generates actual proof evidence: the verifier explores all reachable paths and checks that every
requires/ensurescontract holds. The output is a structured proof object, not a vague "verified" badge. -
Prove check independently replays the proof. This is a separate verification step so you do not have to trust the prover — you trust the checker.
The distinction matters. Older verification tools often collapse these into one fuzzy green checkmark. X07 keeps them separate because different trust claims need different evidence.
Step 8: Certify
Proof is one layer. Certification bundles all the evidence — proof, tests, architecture, boundaries, schemas, trust posture — into one reviewable package.
verified_core_pure_v1 is a strong solve-pure trust profile. Strong profiles require:
--entrymust matchx07.json.operational_entry_symbolcertification_entry_symbolmust be unset (surrogate entries are rejected)- the project must actually be certifiable in the profile’s allowed world(s)
The api-cell scaffold is a run-os-sandboxed service project, so it is not directly compatible with verified_core_pure_v1.
If you are certifying a networked run-os-sandboxed service, start from x07 init --template trusted-network-service and certify under trusted_program_sandboxed_net_v1 instead.
# Bring the built-in profile into your repo (so you can edit its entry allowlist).
mkdir -p arch/trust/profiles
cp .agent/docs/examples/verified_core_pure_v1/arch/trust/profiles/verified_core_pure_v1.json \
arch/trust/profiles/verified_core_pure_v1.json
# Edit arch/trust/profiles/verified_core_pure_v1.json and allowlist your entry symbol:
# "entrypoints": ["orders.core.compute_total_v1"]
# Validate the project against the trust profile first.
x07 trust profile check \
--profile arch/trust/profiles/verified_core_pure_v1.json \
--project x07.json \
--entry orders.core.compute_total_v1
# Bundle all evidence into a certificate.
x07 trust certify \
--project x07.json \
--profile arch/trust/profiles/verified_core_pure_v1.json \
--entry orders.core.compute_total_v1 \
--out-dir target/cert
The output lands in target/cert/:
target/cert/
certificate.json # The structured verdict
summary.html # Human-readable overview
boundaries.report.json # Boundary index validation
tests.report.json # Test execution results
verify.coverage.json # What the verifier covered
prove/ # Per-symbol proof artifacts
trust.report.json # Trust posture summary
compile.attest.json # Compile attestation
Step 9: What the certificate actually says
The certificate.json is the thing a reviewer reads instead of the source tree:
This is an X07 trust certificate. Comments explain what each field means for the review decision.
{
"profile": "verified_core_pure_v1", // Which trust profile was claimed.
"operational_entry_symbol": "orders.core.compute_total_v1", // The actual function being certified.
"formal_verification_scope": "entry_body", // The verifier covered the entry body itself.
"entry_body_formally_proved": true, // The entry was proved, not just its helpers.
"proof_inventory": [
{
"symbol": "orders.core.compute_total_v1", // Symbol that was proved.
"kind": "defn", // It is a pure function definition.
"result_kind": "proven" // Full proof — not bounded or assumed.
}
],
"proof_assumptions": [], // No unproved assumptions were needed.
"accepted_depends_on_bounded_proof": false, // Verdict does not rely on depth-bounded proofs.
"accepted_depends_on_dev_only_assumption": false // No developer-only escape hatches used.
}
That is not vague. It tells the reviewer:
- What profile was claimed —
verified_core_pure_v1means pure, verified core with no OS effects. - What was actually proved — the operational entry body, not a surrogate helper.
- What assumptions were used — none in this case.
- Whether the verdict depends on bounded proofs or dev-only assumptions — it does not.
A reviewer can approve this without reading the function body. The evidence chain is: contracts on the function → proof that the contracts hold for all inputs → independent proof check → certificate that binds the proof to the operational entry. Each link is structured and machine-checkable.
Step 10: The review gate
Before merging, run the review diff to catch trust regressions:
# Produce a semantic diff between the baseline and the candidate.
x07 review diff \
--from baseline \
--to candidate \
--html-out target/review/diff.html \
--json-out target/review/diff.json \
--fail-on proof-coverage-decrease \
--fail-on assumption-surface-widen \
--fail-on bounded-proof-introduced \
--fail-on operational-entry-diverges \
--fail-on sandbox-policy-widen
# Emit a trust summary with budgets, capabilities, and SBOM.
x07 trust report \
--project x07.json \
--out target/trust/trust.json \
--html-out target/trust/trust.html
The --fail-on flags are CI gates. They catch things like: proof coverage went down, a new assumption was introduced, a bounded proof replaced a full proof, the operational entry changed without updating the profile, or the sandbox policy was widened. Those are exactly the trust regressions a human would miss in a code review of generated files.
The full pipeline in one diagram
What this changes about agent-written services
Without this pipeline, reviewing an agent-written service means reading every generated file — the domain logic, the adapters, the configuration, the test fixtures, all of it. That does not scale.
With this pipeline, the reviewer's job changes. Instead of reading source, they read the certificate bundle and the review diff. The questions become:
- Did the operational entry pass formal verification with no bounded proofs or dev-only assumptions?
- Did the test suite — including property-based tests — pass on the full input space?
- Did the architecture check enforce the trust zone boundaries?
- Did the sandbox policy stay within bounds?
- Did proof coverage increase or at least hold steady?
Those are answerable from the artifacts. They do not require the reviewer to understand every line of x07AST JSON.
That is the whole point.
The code can be written by an agent. The evidence that the code is correct can be checked by a human — or by another agent — from the certificate bundle alone.
If you want to try it: