# Capsulang v0.7 — Reference Specification

Status: Editor's Draft
Editor: Capsulang Working Group
Last revised: 2026-05

## Abstract

Capsulang is a language and runtime for AI-authored, human-verifiable systems.
A **capsule** is a self-contained unit of executable intent: typed,
effect-declared, replayable, checkable, and proof-obligation-aware. Capsulang lets humans and AI
systems co-author capsules, while a deterministic parser, checker, interpreter,
and ledger decide what is valid.

This document is the human-readable summary of the spec. The normative editor's
draft is mirrored at `/spec/capsulang-v0.7-standard.md`, and the standard
manifest is mirrored at `/spec/standard_manifest.json`. The page at the project
root is generated from the same data sources under `src/spec/`.

## Semantic Trace

Capsulang records structured semantic trace events alongside replay ledgers. Trace events carry trace/span ids, event kind, component, operation, diagnostic fields, and bounded breadcrumb history. The trace is diagnostic evidence, not the execution-control layer; checked Capsule Core still emits typed effect intents that host adapters may execute.

## Formal Verification

Verification is a ladder: parse, check, execute examples/replay, generate proof obligations, record refinement claims, then discharge them in a trusted verifier or backend comparison harness. `caps emit-lean-obligations` emits V3 theorem obligations for pure functions and structural machine invariants. `caps verify-lean` only succeeds when Lean accepts the proof-complete file and no open proof markers remain. The current proof-complete fixtures cover identity, Boolean negation, integer add-zero postconditions, and a simple machine final-state invariant. `caps refinement-report` checks supported Wasm WAT against examples with i64 wrap semantics, checks selected RISC-V assembly opcode patterns, and keeps proof-grade backend behavior claims explicit while they remain open; `--require-closed` lets CI fail a selected backend slice that still has open, blocked, failed, or unevidenced claims.

## Architecture Plan and Backends

`caps architecture-plan` emits the checked host-facing bindings for stores, surfaces, ports, agents, contracts, and effect targets. The supported pure function subset includes deterministic text, option/result, map, named-function callback helpers, imports, tagged variant, and match semantics. The scalar codegen subset can emit WAT, RISC-V RV64 assembly, Solidity, and Lean definitions, with explicit diagnostics for unsupported aggregate, callback, pattern-match, and backend-specific scalar bodies. Wasm and RISC-V both lower signed `I32`/`I64`/`Int` and unsigned `U32`/`U64` arithmetic/comparisons through type-appropriate signed or unsigned operators; Solidity maps contract-safe scalar widths including `U256`/`Wei` and casts integer literals to the checked operand type. Fixed-width backend behavior remains refinement evidence, not a replacement for the reference interpreter semantics.
## Improvement Governance

Capsulang v0.7 now includes first-class declarations for governed recursive improvement loops: `lineage`, `objective`, `eval-suite`, `successor-contract`, `budget`, `gate`, `deployment-policy`, `improvement-record`, and `verification-hook`. These declarations make AI-generated successors measurable, reviewable, budgeted, gated, rollback-ready, and ledgerable instead of granting direct self-modification authority.

Typed improvement effects such as `llm.call`, `repo.propose_patch`, `ci.run`, `eval.run`, `proof.verify`, `deploy.canary`, `deploy.promote`, `deploy.rollback`, `approval.request`, and `risk.review` remain host-mediated effect intents. CPS-8 `Improvement-Governed` conformance requires implementations to parse, check, canonicalize, and prepare these declarations for runtime policy and ledger evidence.