# Capsulang v0.7 Standard Status: Editor's Draft Last revised: 2026-06-12 ## Scope Capsulang v0.7 defines a checked capsule language for AI-authored, human-reviewable programs. A conforming implementation must treat the deterministic parser, checker, interpreter, ledger, and verification tools as authoritative. Model output is advisory until accepted through those deterministic stages. The standard is split into cumulative conformance levels. Each level includes all lower levels unless a feature is explicitly marked as optional or backend-specific. ## Normative Artifacts - `specs/standard/capsulang-v0.7-standard.md`: this normative prose standard. - `specs/standard/constructs.json`: construct support matrix. - `specs/standard/effects.json`: known effect domains and determinism classes. - `specs/standard/conformance.json`: cumulative conformance levels. - `specs/standard/backend_capabilities.json`: backend codegen coverage, ABI/memory notes, validation hooks, and unsupported feature matrix. - `specs/standard/standard_manifest.json`: artifact index and compatibility policy. Reference web mirrors must publish byte-for-byte equivalent JSON data for the machine-readable artifacts. ## Source Form Capsulang source is an s-expression module. Whitespace is insignificant outside string literals. Implementations must preserve deterministic parsing, diagnostics, canonical IR, and semantic hashes for equivalent source. ```ebnf Module = "(" "module" ModuleName ModuleItem* ")" ; ModuleItem = Capsule | Profile | Import | Type | Enum | Variant | Error | Event | Store | Surface | Port | Agent | Contract | Principal | Mandate | Delegation | Capability | AuthorityPolicy | TrustBoundary | TelemetryObligation | MemoryPolicy | Lineage | Objective | EvalSuite | SuccessorContract | Budget | Gate | DeploymentPolicy | ImprovementRecord | VerificationHook | Function | Machine ; Capsule = "(" "capsule" String ")" ; Profile = "(" "profile" Symbol* ")" ; Import = "(" "import" ModuleName ")" ; Type = "(" "type" Name TypeBody ")" ; Enum = "(" "enum" Name Symbol+ ")" ; Variant = "(" "variant" Name VariantCase+ ")" ; VariantCase = "(" Name Field* ")" ; Error = "(" "error" Name Field* ")" ; Event = "(" "event" Name Field* ")" ; Store = "(" "store" Name StoreClause* ")" ; Surface = "(" "surface" Name SurfaceClause* ")" ; Port = "(" "port" Name PortClause* ")" ; Agent = "(" "agent" Name AgentClause* ")" ; Contract = "(" "contract" Name ContractClause* ")" ; Principal = "(" "principal" Name PrincipalClause* ")" ; Mandate = "(" "mandate" Name MandateClause* ")" ; Delegation = "(" "delegation" Name DelegationClause* ")" ; Capability = "(" "capability" Name CapabilityClause* ")" ; AuthorityPolicy = "(" "authority-policy" Name AuthorityPolicyClause* ")" ; TrustBoundary = "(" "trust-boundary" Name TrustBoundaryClause* ")" ; TelemetryObligation = "(" "telemetry-obligation" Name TelemetryClause* ")" ; MemoryPolicy = "(" "memory-policy" Name MemoryPolicyClause* ")" ; Lineage = "(" "lineage" LineageClause* ")" ; Objective = "(" "objective" Name ObjectiveClause* ")" ; EvalSuite = "(" "eval-suite" Name EvalSuiteClause* ")" ; SuccessorContract = "(" "successor-contract" Name SuccessorRule* ")" ; Budget = "(" "budget" Name BudgetClause* ")" ; Gate = "(" "gate" Name GateClause* ")" ; DeploymentPolicy = "(" "deployment-policy" Name DeploymentPolicyClause* ")" ; ImprovementRecord = "(" "improvement-record" Name ImprovementRecordClause* ")" ; VerificationHook = "(" "verification-hook" Name VerificationHookClause* ")" ; Function = "(" "function" Name FunctionClause* ")" ; Machine = "(" "machine" Name MachineClause* ")" ; Expression = Literal | Symbol | Field | Call | If | Let | Op | Record | VariantConstructor | List | Map | Match | Sum | Fold | Convert | Old ; ``` This grammar is intentionally abstract. The reference parser defines the exact accepted v0.7 subset, and any implementation claiming CPS-0 must match its accepted and rejected fixture behavior. The reference parser reserves unquoted symbols beginning with `0x` for hex literal parsing and unquoted symbols containing `.` for field access shorthand. Such tokens are not available as ordinary variable names in v0.7 source. Protocol-facing architecture declarations are additive in v0.7: - `surface` supports A2UI protocol metadata through `(protocol a2ui "v0.9")`, `(catalog "...")`, typed `(state field*)`, and typed `(action Name ...)` declarations. Actions may declare input payload fields, required user confirmation, required auth scopes, and metadata effects. - `port` supports MCP protocol metadata through `(protocol mcp "2025-11-25")`, rich `(tools (tool ...))`, `(resources (resource ...))`, and `(prompts (prompt ...))` declarations. The older shorthand `(tool name...)` remains valid. - `agent` supports A2A protocol metadata through `(protocol a2a "1.0")`, `(discovery ...)`, `(auth scheme scope*)`, and rich `(skills (skill ...))` declarations. The older shorthand `(skill name...)` remains valid. `input` and `output` payload clauses in protocol declarations may name an existing type or provide inline fields. Protocol declarations describe host adapter contracts; they do not execute adapters or grant ambient authority by themselves. ## Static Semantics Implementations at CPS-1 or higher must reject a module before execution when any of these conditions holds: - syntax is invalid or a required declaration clause is missing; - names resolve ambiguously or do not resolve; - expressions have incompatible input, output, guard, assignment, or postcondition types; - match expressions contain unknown/duplicate cases, invalid payload bindings, or miss a case without an `else` arm; - imported modules do not resolve from explicit implementation roots, resolve to a different module name, or form an import cycle; - function bodies infer undeclared positive effects; - profiles forbid declared or inferred effects; - architecture effect targets reference missing stores, surfaces, ports, agents, tools, resources, A2UI actions, or skills; - Authority IR references between principals, mandates, delegations, capabilities, gates, effect targets, trust boundaries, telemetry obligations, and memory policies are inconsistent or incomplete; - machine transitions target missing states or violate event/guard/assignment requirements; - improvement governance declarations reference missing objectives, eval suites, contracts, gates, budgets, proof targets, or invalid hash/status/operator/effect names; - deploy.* improvement effects appear without a deployment policy plus an eval-suite gate and approval gate; - cyclic type aliases appear in the nominal type graph. Warnings, such as unreachable machine states or missing terminal handling, must not be reported as successful checks unless the diagnostic severity remains distinguishable from errors. ## Dynamic Semantics Pure function evaluation is deterministic and side-effect free. Integer `/` and `mod` use truncation-toward-zero semantics. The reference interpreter evaluates integer arithmetic with arbitrary-precision host integers; fixed-width backends such as Wasm or RISC-V may wrap, trap, or otherwise diverge on overflow unless a checked refinement claim explicitly covers the boundary case. Machine execution is event-driven: a runtime computes a transition plan, validates effect targets, and then routes declared effects through mode-aware adapters. Text operations are deterministic and locale-free. `text.concat` concatenates two or more `Text` values. `text.length` returns a `U64` Unicode code-point count. `text.slice` uses zero-based start-inclusive, end-exclusive indexes and requires `0 <= start <= end` at runtime. `text.contains` returns whether the second `Text` argument is a substring of the first. `text.format` replaces `{}` placeholders left-to-right, supports escaped braces with `{{` and `}}`, and renders `Text`, `Bool`, `Unit`, and numeric values without locale-sensitive formatting. Option and result helpers are deterministic and expected-type driven where a constructor would otherwise be under-specified. `option.some` and `option.none` construct `Option` values, `option.is-some` tests presence, `option.unwrap-or` returns the contained value or a default, and `option.map` maps present values through a checked one-argument function reference. `result.ok` and `result.err` construct `Result` values, `result.is-ok` tests success, `result.unwrap-or` returns the ok value or a default, `result.map` maps ok values, and `result.map-err` maps error values. `option.none`, `result.ok`, and `result.err` must be checked against an expected `Option` or `Result` type supplied by the surrounding expression, function output, example input, or branch context. Map literals use `(map (key value)...)` and must have compatible key/value types, or an expected `Map` type for empty maps. `map.get-or` must return the stored value when the key exists and otherwise return the explicit default. `map.put` must return an updated map value without mutating the original map. `map.merge` is right-biased: keys from the second map replace keys from the first map. `map.filter` evaluates a checked predicate function with each key/value pair and preserves entries whose predicate result is true. Runtime map keys are scalar values so rendering and equality remain deterministic. Enums and tagged variants are nominal types. Enum and variant values are constructed with `(Type.Case (field expr)...)`; enum cases do not accept payload fields. A tagged variant declaration uses `(variant Name (Case field*)...)`. `match` evaluates one arm from left to right by the subject case and may bind payload fields into local names. The checker must reject unknown cases, duplicate cases, payload bindings for fields that do not exist on the selected case, and non-exhaustive matches unless an `else` arm is present. `match` is defined for enums, tagged variants, options (`some`/`none`), and results (`ok`/`err`). Machine timeout transitions use `(after DurationExpr ...)` within a state. The duration expression must be pure and evaluate to a nonnegative integer millisecond delay. Implementations must schedule timeout transitions deterministically by `(delay_ms, transition_index)` for the active state. The reference runtime represents firings as synthetic events: `@timeout` fires the earliest scheduled timeout, and `@timeout:state:index` fires an explicit scheduled timeout. Ledgers must record timeout schedules and timeout firings as replayable data; replay must not consult ambient wall-clock time. Normal transitions cancel scheduled timeout events from the exited snapshot unless the same synthetic timeout remains scheduled with the same delay in the next snapshot. Ledgers must record those cancellations so stale timeout deliveries can be rejected by replay. Effectful transitions may declare `(retry (max N) (backoff DurationExpr))`, `(on-error State)`, and `(compensate Effect...)`. Retries are deterministic attempt metadata: the runtime does not sleep or read wall-clock time, and retry backoff is recorded as a nonnegative millisecond value. If an effect fails after retries and no `on-error` target exists, the transition is unhandled and the snapshot is not committed. If `on-error` exists, the runtime records the diagnostics, runs compensation effects, and commits the transition to the failure target with the planned context. Replay must use ledgered failure decisions and effect outcomes rather than re-executing external effects. Runtime modes have distinct obligations: - `dry-run`: produce explicit planned effect outcomes without network or database I/O. - `mock`: dispatch only to configured mock handlers. - `live`: dispatch only to configured live handlers or adapter bundles. The bundled HTTP and MCP adapter clients are lightweight reference transports for conformance tests, demos, and local integration. They are not production-grade network clients; production hosts should provide hardened transports with their own connection management, observability, TLS policy, and retry budgets behind the same runtime adapter boundary. External effects are data until a host adapter executes them. A conforming runtime must not invent ambient authority outside declared effects and runtime policy. Runtime policy may restrict effect names, effect targets, endpoint protocols, endpoint hosts, and secret sources. A live runtime must evaluate configured policy before invoking adapter handlers. Secret material in runtime configuration should be referenced through configured providers, such as environment variable references, instead of embedded in source modules. Runtime operations may configure per-effect-target circuit breakers. When a circuit is open, the runtime must deny the effect before adapter handler execution and report a structured diagnostic. ## Agentic External Interfaces Capsulang is protocol-native at the host boundary: ```text MCP = capsule runtime to tools, data, and resources A2A = capsule runtime to collaborator agents A2UI = capsule runtime to user-facing dynamic interfaces ``` The language layer declares protocol contracts and typed effect intents. The host runtime owns transport hardening, authentication, credential isolation, adapter execution, UI rendering, and audit persistence. Known protocol effects are: - `mcp.call port.tool` - `mcp.read-resource port.resource` - `mcp.subscribe-resource port.resource` - `a2a.message agent` - `a2a.task agent.skill` - `a2a.receive-artifact agent.artifact` - `a2ui.emit surface` - `a2ui.update-data surface.path` - `a2ui.await-action surface.action` - `requires-user-confirmation` - `requires-auth scope` - `uses-untrusted-external-data` The checker validates that protocol effect targets resolve to declared ports, resources, agents, skills, surfaces, and actions. Runtime dry-run mode records these effects as planned intents; live mode dispatches only through configured adapter handlers or adapter bundles. MCP and A2A results and A2UI action payloads must be treated as untrusted external data until a capsule or host validation step accepts them. A2UI envelopes are declarative JSON messages with media type `application/json+a2ui`. The reference implementation emits `createSurface`, `updateComponents`, `updateDataModel`, and `deleteSurface` envelopes from declared surfaces. A host renderer must render them through a trusted component catalog and dispatch returned actions as typed events or policy-checked effect intents. `python -m capsulang protocol-plan ` emits the host-facing MCP, A2A, and A2UI binding plan. `python -m capsulang a2ui-manifest ` emits the A2UI surface/action/catalog manifest. `python -m capsulang a2ui-envelope Surface --kind create|components|data|delete` emits one deterministic A2UI envelope for a declared surface. The React target is the reference A2UI UI target. `python -m capsulang compile --target react --out ` emits React components, TypeScript surface/action types, host bindings, the protocol plan, the A2UI manifest, and deterministic envelope fixtures. Generated React is a renderer and event bridge only; host policy, credentials, adapters, telemetry, ledger writes, and effect execution remain outside the target. ## Authority IR Semantics Authority IR declarations describe the authorization and accountability envelope around effectful capsules. They are first-class module items but deliberately do not grant ambient authority. A conforming implementation must parse, check, canonicalize, print, and export the Authority IR subset deterministically. A live host remains responsible for identity-provider integration, credential issuance, runtime ABAC/JIT policy, sandbox/container enforcement, adapter execution, and SIEM/ledger persistence. The Authority IR subset consists of: - `principal`: an accountable actor, such as a human, organization, service, or agent. Agent principals should use cryptographic identity and non-static credentials. - `mandate`: a bounded reason why a principal may act, including issuer, recipient, purpose, subjects, scopes, validity, and revocability. - `delegation`: a scoped, revocable handoff of authority from one principal to another under a mandate. - `capability`: a short-lived action right bound to a principal and declared effect intent. Capabilities may depend on mandates, delegations, approvals, limits, risk class, and revocation policy. - `authority-policy`: a typed decision surface whose outcomes are normally `allow`, `deny`, `defer`, and `escalate`. - `trust-boundary`: sandbox, network, filesystem, egress, secrets, attestation, and capability requirements for the execution environment. - `telemetry-obligation`: required telemetry events, attribution fields, export sinks, and tamper-evidence metadata. - `memory-policy`: isolation, TTL, source attribution, hash validation, quarantine, and promotion rules for persistent agent memory. A checked module may emit typed effect intents and Authority IR. The runtime must still mediate live effects through host policy and adapters. This preserves the core boundary: Capsulang checks executable intent; the host authorizes and executes external consequences. `python -m capsulang authority-ir ` emits the machine-readable Authority IR subset with `schemaVersion: 1` and `kind: capsulang.authority_ir`. ## Improvement Governance Semantics Capsulang supports governed recursive self-improvement workflows without granting unbounded self-modification authority. Improvement declarations are first-class module items that describe a proposed successor, the objective it is allowed to optimize, the evaluations and proofs it must satisfy, the authority budget it may consume, and the gates that must pass before deployment. The governance layer is deliberately evidence-oriented: - `lineage` records parent and candidate semantic hashes, proposer identity, timestamp, and reason. - `objective` gives the improvement loop measurable metrics, optimization directions, and constraints. - `eval-suite` declares datasets, thresholds, and required examples, replay, property, red-team, or proof checks. - `successor-contract` declares cross-version preservation, prohibition, and required-evidence rules. - `budget` bounds iterations, calls, CI runs, wall-clock, cost, and effect allow/deny sets. - `gate` declares evidence requirements and pass/fail actions such as quarantine, canary, or rollback. - `deployment-policy` describes shadow, canary, live, rollback, promotion, and quarantine behavior. - `improvement-record` is the ledger-ready summary of parent/candidate/diff hashes, eval/proof results, policy decisions, approvals, deployment outcomes, and rollback pointer. - `verification-hook` exposes improvement proof obligations to Lean, policy engines, or trusted external verifiers. Typed improvement effects are external authority requests and must remain data until a host adapter approves and executes them. The known improvement effect domains are `llm.call`, `repo.diff`, `repo.propose_patch`, `repo.apply_patch.sandboxed`, `ci.run`, `eval.run`, `proof.emit`, `proof.verify`, `model.finetune`, `model.eval`, `deploy.shadow`, `deploy.canary`, `deploy.promote`, `deploy.rollback`, `approval.request`, and `risk.review`. A capsule must not be considered improvement-governed merely because it can edit or deploy code. CPS-8 requires that candidate successors are compared by canonical hash, checked against objectives and successor contracts, evaluated before promotion, constrained by budgets, gated by explicit evidence, and recorded in a replayable improvement record. Example: ```lisp (lineage (parent "sha256:aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa") (candidate "sha256:bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb") (reason "Improve claim triage while preserving authority boundaries.")) (objective BetterTriage (metric f1_score "evals/claim_triage_gold.jsonl") (maximize f1_score) (constraint live_effects_added == 0)) (eval-suite ClaimReviewRegression (dataset "evals/claim_review_regression.jsonl") (metric exact_match >= 98) (must-pass examples) (must-pass replay "ledgers/golden/*.jsonl")) (successor-contract SafeSuccessor (preserve contract:NoUnauthorizedEffects) (forbid effect-expansion unless approval:SecurityOwner) (require eval-suite:ClaimReviewRegression)) (gate DeployCandidate (requires eval-suite ClaimReviewRegression passed) (requires successor-contract SafeSuccessor preserved) (requires approval SecurityOwner) (on-fail quarantine) (on-pass canary)) ``` ## Canonical IR And Hashing Canonical IR is deterministic JSON with stable ordering. Semantic hashes are computed from canonical IR, not source text. Implementations claiming compatibility with the reference implementation must reproduce semantic hashes for conformance fixtures at the same standard version. Import declarations, protocol-facing architecture declarations, Authority IR declarations, and improvement-governance declarations are part of canonical IR. An importing module records each imported module name and the imported module semantic hash. Implementations must resolve imports from explicit roots and must reject cycles before computing a successful checked result. ## Verification Semantics The standard distinguishes checked from verified. A checked capsule passed parser, type, effect, architecture, and example/replay checks. A verified capsule also has configured proof obligations accepted by a trusted verifier with no open proof markers. `caps emit-lean-obligations` and `caps verify-lean` define the reference Lean path. Generated theorem stubs are obligations, not proofs. The current reference proof fixtures cover identity, Boolean negation, integer add-zero postconditions, and a simple machine final-state invariant with a small standalone Lean support prelude plus generated finite-state machine models. Same-state/same-event machine branches use generated branch event constructors so structural Lean models preserve each edge while guard semantics remain assumptions. Generated Lean constructor-name collisions are reported as open obligations rather than left to downstream Lean errors. `caps refinement-report` defines the V5 evidence surface for AST/IR, interpreter, backend artifact, Wasm emitted-WAT example comparison with i64 wrap semantics, RISC-V static assembly-pattern checks, and open backend-behavior refinement claims. ## Backend Code Generation Backends are implementation artifacts, not alternate language definitions. Parser, checker, interpreter, machine runtime, ledger, and verification policy remain authoritative. A conforming backend report must identify the target backend, generated artifact, supported functions or machines, unsupported declarations, diagnostics, ABI conventions, memory conventions, and validation status. Unsupported features must produce explicit diagnostics or explicit skip markers; implementations must not silently claim support for unimplemented behavior. The v0.7 reference backend matrix is `specs/standard/backend_capabilities.json`: - Wasm text and RISC-V RV64 cover pure scalar functions over supported integer and Bool types. Wasm maps Bool to `i32` and integer-like values to `i64`; signed `I32`/`I64`/`Int` and unsigned `U32`/`U64` select signed or unsigned Wasm operators. RISC-V uses the RV64 integer ABI with up to eight integer arguments in `a0`-`a7` and result in `a0`; signed integers use `div`/`rem`/`slt`, while unsigned integers use `divu`/`remu`/`sltu`. Tagged variants and `match` require aggregate layout work and are explicit unsupported expressions for these scalar backends. - Solidity covers the deterministic contract-safe pure subset over `Bool`, `Text`, `Address`, signed `I32`/`I64`/`Int`, and unsigned `U32`/`U64`/`U256`/`Wei` scalar values. Integer literals in arithmetic and comparisons must be cast to the checked operand type so Solidity's signed/unsigned and checked-overflow behavior is explicit. `Bytes32`, `Json`, `Timestamp`, `Duration`, `QName`, and `Probability` remain unsupported until a stable contract ABI is defined. Live adapter effects must stay outside generated contract behavior. - Lean output is a proof artifact, not a runtime ABI. Unsupported definitions must remain visibly open as obligations or axioms. - XState and SCXML cover checked machine topology and metadata for guards, assignments, effects, retries, timeouts, and failures. Host runtime code remains responsible for evaluating expressions and executing effects. Toolchain validation is optional and environment-dependent. A missing validator is reported as `skipped`; a present validator failure is a backend validation diagnostic. ## Compatibility Policy - Syntax extensions within v0.7 must be additive or feature-gated. - Breaking semantic changes require a new standard version. - Diagnostic codes are stable within a minor line unless explicitly deprecated. - Canonical IR includes protocol-facing architecture declarations, Authority IR declarations, and improvement-governance declarations in v0.7; semantic hash changes require a compatibility note and conformance fixture update. - Backend codegen may be partial, but unsupported features must produce explicit diagnostics or skip markers. ## Conformance Conformance levels are defined in `specs/standard/conformance.json`. CPS-0 through CPS-10 are cumulative. Implementations may claim a backend-specific subset only when the claim identifies the backend, the supported constructs, and the fixture pack used to validate the claim.