Unified CLI v1: review, verify, agent, query, package, add, and fetch

September 13, 2026 · View on GitHub

Status: implemented bounded profile; HOSTED GREEN under the v0.4.0 release baseline. Historical local, authoring-time, ignored, device/simulator, or separately provisioned evidence below retains its narrower scope; public promotion, registry publication and broader product completion remain separately gated.

Audience: SEMAPRAX users, coding agents, editor and tooling authors, and compiler contributors.

Purpose

The 1.0 command surface converges public workflows on one semaprax binary and a short list of verbs. These verbs front capabilities the compiler already had under protocol-specific names or library APIs. They select and delegate; they add no semantic validation or authority of their own.

`semaprax review`

semaprax review <file> <patch.spatch>
semaprax review <project> <transaction.json> [--evidence]

The first form remains the byte-preserved Bounded Semantic Review v1 workflow. The additive Project form authenticates the selected Project for the complete invocation, opens one process-local SemanticWorkspaceService, and passes the transaction file's exact bytes to validate_transaction. The transaction must therefore be the canonical, revision-bound closed Universal Semantic Transaction v1 envelope; stale, malformed, noncanonical, unsupported, and oversize inputs retain the transaction kernel diagnostics, while the service's active-generation precheck owns stale revision SPX-G530.

Ordinary success prints the exact SemanticTransactionArtifacts::review() bytes. --evidence prints the exact SemanticTransactionArtifacts::evidence() bytes, which digest-bind the intent, impact, review, and complete validation result. The adapter introduces no wrapper or competing result schema. The grammar is closed: --evidence is the only option, is admitted only once and only on the Project form, and no stdin, implicit transaction construction, or old-revision retrieval is admitted.

This workflow reads explicitly selected local inputs and derives an in-memory candidate. It does not change source, write a candidate or cache, stage, apply, commit, publish, pivot ACTIVE, approve a change, or grant reusable authority. The evidence is proof data, not permission. It is not a daemon, shared service, transport, editor session, behavioral-equivalence proof, runtime execution, or general transaction algebra; Universal Semantic Transaction v1's operation and comment-free canonical-source limits remain unchanged.

`semaprax verify`

semaprax verify <subject> <change> <capsule.json>
semaprax verify <manifest> <image.json>

The last operand is always the capsule to replay. The front reads it once, takes its top-level string schema, and selects the verifier that owns that schema for that operand count. It then hands the same paths, unchanged and in the same order, to that verifier, which re-reads and independently replays them exactly as the long-form route does. The receipt is the verifier's own bytes; the front never rewrites, wraps, or summarizes it.

Capsule schema	Operands	Verifier
`semaprax.semantic-patch-evidence.v1`	`<file> <patch.spatch> <capsule>`	`verify-patch-evidence` (Semantic Patch Evidence v1)
`semaprax.semantic-patch-evidence.v2`	`<file> <patch.spatch> <capsule>`	`verify-patch-evidence-v2` (Semantic Patch Evidence v2)
`semaprax.semantic-workspace-patch-evidence.v1`	`<root> <patch.wspatch> <capsule>`	`verify-workspace-patch-evidence` (Semantic Workspace Patch Evidence v1)
`semaprax.workspace-semantic-change-evidence.v1`	`<root> <proposal.json> <capsule>`	`verify-semantic-workspace-change-evidence` (Semantic Workspace Change v1)
`semaprax.workspace-semantic-structural-change-evidence.v1`	`<root> <proposal.json> <capsule>`	`verify-semantic-workspace-structural-change-evidence`
`semaprax.semantic-workspace-operations-evidence.v1`	`<root> <proposal.json> <capsule>`	`verify-semantic-workspace-operations-evidence` (Semantic Workspace Operations v1)
`semaprax.agent-graph.v1`	`<definition.json> <profile.json> <graph.json>`	`agent_definition::verify_agent_graph_bundle` (Language-Native Agent Object v1)
`semaprax.semantic-workspace-image.v1`	`<manifest> <image.json>`	`project-image-verify` (Semantic Workspace Image v1)

The agent graph bundle is the one route without a long-form command. On success it prints one receipt line:

{"schema":"semaprax.agent-graph-verification.v1","agent_id":"...","definition_digest":"sha256:...","graph_digest":"sha256:...","verified":true,"authority":false}

The identities and digests come from an independent recompilation of the definition after the bundle comparison passed; the receipt asserts equality of bytes, not fitness of the agent.

Fail-closed selection

Selection happens before any verifier runs, so a rejected capsule leaves no verifier receipt and no side effect:

Code	Meaning
`SPX-V201`	The capsule's schema is admitted for no verifier at this operand count. The message lists the schemas admitted for that count.
`SPX-V202`	The capsule cannot be read, exceeds 16 MiB, is not a JSON document, or has no top-level string `schema`.

A capsule whose schema selects a verifier but whose contents that verifier rejects produces exactly the long-form route's diagnostics and status; the front adds nothing. The grammar is closed: two or three operands, none empty and none starting with -; anything else exits with status two.

Non-claims

verify performs no verification itself, does not authenticate the capsule beyond reading schema, does not apply, publish, or lock anything, and does not introduce a new evidence format. Evidence capsules still carry no authority (AGENTS.md); a passing verify is proof data for the route that owns it, nothing more.

`semaprax agent`

semaprax agent inspect <definition.json> [--profile]
semaprax agent run <definition.json> <task.json> <transcript.json> [--evidence|--trace]
semaprax agent replay <definition.json> <task.json> <transcript.json> <evidence.json>

agent is the 1.0 verb for the agent lifecycle. Three subcommands are admitted, each a pure function of its input documents that grants no provider, tool, filesystem, process, network, clock, approval, or publication authority.

inspect compiles a canonical AgentDefinition v1 document through agent_definition::compile_agent_definition and prints the deterministic AgentGraph v1 canonical JSON (the compiler's projection, including its terminal LF), or the byte-preserved Agent Runtime Profile v1 projection with --profile. Diagnostics are the agent compiler's own (SPX-G501, SPX-G502); an unreadable file reports SPX-I001.

run compiles the definition, derives its Runtime v1 profile, and executes one canonical semaprax.agent-runtime-task.v1 document through the bounded runtime against a scripted host. The host is the transcript:

{"schema":"semaprax.agent-runtime-transcript.v1","policy_epoch":7,
 "provider":[{"disposition":"succeeded","response":"{\"schema\":\"semaprax.agent-runtime-action.v1\",...}\n"},
             {"disposition":"definitely_not_started"},{"disposition":"failed_uncertain"}],
 "tools":[{"result":"{\"value\":\"alpha\"}"},{"result":null}]}

Provider attempts and tool invocations consume the two arrays in order; a succeeded attempt streams its response bytes, an exhausted provider script answers failed_uncertain, and a null or exhausted tool script fails the invocation. Elapsed time is always zero and the policy epoch is the transcript's, so every observation the runtime makes is a function of the three documents and the run is deterministic. The transcript is a closed object of at most 4 MiB and 256 entries per array; anything else reports SPX-V221. By default run prints one receipt line naming the agent, the terminal status (completed, cancelled, deadline_exceeded, budget_exhausted, provider_failed, tool_failed, policy_rejected), the final message or null, and the trace and evidence digests; --evidence prints the canonical semaprax.agent-runtime-evidence.v1 document instead and --trace the semaprax.agent-runtime-trace.v1 document. A run that ends in a runtime failure status is still a successful invocation; only rejected input documents exit with status one.

replay re-runs the same three documents and requires the recomputed evidence to equal the supplied capsule byte for byte, printing a semaprax.agent-replay-receipt.v1 line with verified: true; any difference is SPX-V222. Nothing in the capsule is trusted, so a replay proves that this compiler, this definition, this task, and this transcript produce exactly this evidence.

resume and reconcile are not admitted: the runtime's non-claims exclude durable memory, persistence, recovery, and resume, and the verb rejects them with a usage error that names the three admitted forms.

`semaprax query`

semaprax query <file|project> [--kind <kind>[,<kind>]] [--name <text>] [--id <prefix>]
                      [--effect <effect>] [--calls <stable-id>] [--called-by <stable-id>] [--json]

query selects declarations of one checked module or one authenticated Project from the documentation model of Documentation Projection v1. Every match carries the identity and canonical signature doc renders. A Project match additionally names its canonical source path, module, and source revision, while the result binds the exact Project and semantic-graph revisions. Filters are a conjunction:

Filter	Holds when
`--kind`	the declaration's kind is one of the listed kinds: `record`, `variant`, `class`, `method`, `resource`, `interface`, `protocol`, `implementation`, `function`
`--name`	the display name contains the text
`--id`	the stable identity starts with the prefix
`--effect`	the declaration's `uses` clause names the effect
`--calls`	the declaration calls the named persistent callable
`--called-by`	the named persistent callable calls the declaration

Call relations come from the persistent call index that impact and the use, so --calls is "semantic references" by stable identity, not a text search. Project queries use the already authenticated cross-file graph, so a library declaration can name callers in entry and test modules without reading the full graph. Without --json, a file query prints kind, identity, and canonical header; a Project query prepends the owning path. --json prints semaprax.query.v1 for a file or semaprax.project-query.v1 for a Project. The Project result includes its revisions and each match's path, module, source revision, kind, identity, name, persistence, signature, location (the one-based line and column followed by the start and end byte offsets of the name token, encoded as a four-integer array to keep the Project result compact), effects, callees, and callers. The VS Code adapter's go-to-declaration, callers, and code-lens features use the single-file route (VS Code adapter).

The query fails closed rather than matching nothing: an unknown kind reports SPX-V211, and an unknown --calls/--called-by identity reports SPX-V212. SPX-V213 names an impossible mismatch inside an already authenticated Project query. A file query still follows no use lines and still requires a standalone checked module; Project inspection must select its directory or manifest. Neither route performs writes or grants source authority.

`semaprax package`

semaprax package report <file> [--max-bytes N]
semaprax package lock <subject.json>... [--max-bytes N]
semaprax package resolve <subject.json>... --require <package>:<range> [--require ...] --target <native64|wasm32> [--allow-capability <capability>]... [--max-bytes N]

package is the 1.0 namespace over the offline package routes. Each subcommand is rewritten to its long-form command (package-report, package-lock, package-resolve) with the same operands and re-enters the dispatcher, so stdout, stderr, and status are the owning route's own; the grammar, bounds, and diagnostics of Package Report v1, Offline Package Lock v1, and Offline Package Resolver v1 are unchanged. The usage recovery hint printed after a rejected invocation names the verb as typed (semaprax package --help), which is the one line that differs from the long form. A missing or unknown subcommand exits with status two before any route runs. add and fetch are not admitted by this revision.

`semaprax add`

semaprax add <dir>|semaprax.toml <package> <range>

add appends one [dependencies] row to a Package Manifest v1 table manifest (Package Manifest v1). It parses the manifest, inserts the row in strict byte order, renders the canonical table layout, and re-parses the result before its one write, so a rejected package identity or range surfaces as the manifest's own SPX-J100 and the file is untouched. A frozen semaprax.project.v* manifest has no [dependencies] table and is rejected with SPX-J127, which names project-scaffold --layout tables; a dependency already present is also SPX-J127. add fetches, resolves, and contacts nothing; the next steps stay explicit (fetch, then resolve).

`semaprax fetch`

semaprax fetch <cache-dir> <subject.json>...

fetch is the caller-populating step Project Dependency Resolution v1 leaves outside the compiler's implicit actions. Each operand is a Semantic Package Subject-v3 envelope file (at most the resolver's subject size). Every subject is independently replayed through the same verifier the resolver uses before anything is written; its cache address is <hex>.json for its own digest sha256:<hex>. An operand that fails replay, carries a non-canonical digest, or would overwrite an entry holding different bytes rejects the whole run with SPX-J128 before any write; an identical entry is reported as present. The cache directory is created when missing and may not exceed the resolver's 64-subject bound. One receipt line is printed:

{"schema":"semaprax.fetch-receipt.v1","cache":"cache","subjects":[{"package":"examples.meaning","version":"1.0.0","digest":"sha256:...","state":"added"}]}

fetch reads only the paths it is given. It performs no network access, no registry lookup, no version selection, and no build; resolve remains the only reader of the cache and still replays every subject itself.

Guided help

The guided page lists review and verify under Change by meaning, query under Inspect meaning, and agent inspect under a new Agents group; package, add, and fetch appear in the exhaustive catalog only. Both capability pages stay within the 2048-byte bound of Guided CLI Help v4; the shapes and several summaries were shortened to make room, and the exhaustive catalog remains the grammar authority.

Executable gates

tests/workspace/unified_review_cli.rs (workspace harness): the Project form prints the exact transaction review and evidence artifacts and leaves every input byte unchanged; noncanonical and stale transactions retain kernel diagnostics; unknown, repeated, and misplaced options fail as usage; scoped help pins both forms. The existing semantic harness continues to pin the single-file form's exact API bytes plus one LF.
tests/semantic/verify_front.rs (semantic harness): for patch evidence v1 and v2, workspace patch evidence, semantic workspace change evidence, and a project image, the verify receipt is byte-identical to the long-form route's; a v2 capsule handed to the v1 subject reproduces the owning verifier's rejection exactly; wrong operand counts, foreign schemas, schema-less documents, non-JSON, and missing capsules fail closed with SPX-V201/SPX-V202 and no stdout; the source is unchanged afterwards.
tests/agent_runtime_v1/agent_inspect_cli.rs (agent runtime harness): agent inspect prints the exact AgentGraph v1 bytes and, with --profile, the exact profile bytes of the library compiler; verify over the definition, profile, and graph prints the receipt with the pinned digests; a tampered graph fails with SPX-G503; agent run follows a tool-then-final transcript to a completed receipt, prints deterministic evidence and trace documents, reports an exhausted script as provider_failed, and rejects malformed transcripts with SPX-V221; agent replay verifies the printed evidence and rejects a tampered capsule with SPX-V222; resume, reconcile, and malformed grammars exit with status two.
tests/projections/query_projection.rs (projections harness): filters select by kind, name, identity prefix, effect, callers, and callees on the committed examples; authenticated Project queries find library declarations, owning paths and cross-file entry/test callers while a raw library file keeps SPX-T105; the exact calculator result stays below 1 KiB, 256 lexical units, and one eighth of its full Project graph; directory and manifest selectors print the library's same one-line JSON; unknown kinds and identities fail closed with SPX-V211/SPX-V212; malformed grammars exit with status two.
tests/offline_package/package_namespace.rs (offline-package harness): every package subcommand's stdout, stderr, and status equal its long form's, and a missing or unknown subcommand exits with status two.
tests/project/add_fetch_v1.rs (project harness): add appends byte-sorted rows that re-parse canonically through both operand forms and leaves the manifest untouched on duplicate, grammar, frozen-layout, and missing-file rejections; fetch files replayed subjects by digest with an exact receipt, reports refetches as present, feeds resolve directly, and rejects tampered, foreign, missing, and colliding subjects before any write.
Unit tests pin the closed grammars, the route table, and the namespace map.

`semaprax network-run`

semaprax network-run [<dir>|semaprax.toml|--manifest-path path] \
  --fixture fixture.json [--arg UTF8]... [--stdin path] [--max-steps N]

network-run is the deterministic execution verb for the exact Project v12 network-command-io.v1 profile. It authenticates the Project, injects one bounded semaprax.network-fixture.v1 provider, and executes the manifest's selected command. It never constructs the TCP provider and therefore never opens a socket. The fixture is limited to 1 MiB and eight connections; combined argv/stdin remains limited to 65,536 bytes. Successful true writes the settled success-only transcripts and exits zero; false exits one, and all failed outcomes publish no transcript.

Compact semantic views

semaprax compact provides read-only dictionary projections and independently checked reconstruction through the existing compact projection codec:

semaprax compact graph <file|project> [--encoding text|binary]
semaprax compact context <file> <stable-id> [--max-bytes N]
semaprax compact task-context <file> <stable-id> [--max-bytes N] [--max-tokens N]
semaprax compact api-surface <project>
semaprax compact candidate-diff <project> <recovery-capsule.json>
semaprax compact agent-definition <definition.json>

Every form admits --encoding text|binary (text by default) and --replay <encoded-file>. Without replay, stdout contains exactly the compact wire bytes. With replay, the command regenerates the selected view, verifies wire integrity and exact profile/root/revision binding, compares reconstructed content, then writes the full ordinary semantic view. Stale or self-rehashed alternate content fails closed; replay grants no write or commit authority. The encoding flag describes both the emitted format and the replay input.

graph accepts either a single checked source or an authenticated Project's full graph. Both use the full-graph profile; the reconstructed graph's schema identifies its original semantic object, and its source revision is respectively the graph revision or Project revision. api-surface is specifically the Project v8 owned-data descriptor. Candidate capsules are restored against the live authenticated Project before selection. Agent definitions are compiled from explicitly supplied bytes. No compact index becomes an operation identity.

Context uses forward depth one and at most 256 nodes; its default byte limit is 65,536. Task context creates one explicit root seed and delegates selection to the goal-aware compiler. Its default budget is 65,536 byte-v1 units, not model tokens. CLI --max-tokens changes that explicitly named accounting budget; model-token savings are measured separately by the benchmark helper.