EVIDENCE · 933196B · 2026-10-15

What v0.9.0 implements, and what it does not prove.

Evidence has a state, a scope, and an expiry date.

Version 0.9.0 resolves to commit 933196b and was published on 11 October 2026 after 91 publication-run jobs passed. The 15 October review covers released installers, five native targets, routing contracts, diagnostic improvements and separately scoped source additions. The ledger distinguishes executable slices, local measurements and still-pending gates.

semaprax://evidencev0.9.0

entity     Semaprax
status     beta
snapshot   933196b
authority  github.com/wavect/semaprax

What does Semaprax implement today?

The beta ships five native archives and verified installer journeys. Its tagged source includes checked semantic edits, source laws, typed runtime Agents, selected Rust and Wasm boundaries, policy-first routing, protected harness workflows and bounded command/data profiles. The full-goal matrix remains 55 Partial, 0 Implemented, 0 Missing. Learned routing is not qualified, native Project tests retain a pending current-head gate, and public generic support remains unsupported and unpublished.

Capability evidence ledger

Full product status 55 Partial · 0 Implemented · 0 Missing

PartialCanonical source and stable identity
PartialBounded context and compact projections
PartialSemantic edits, not arbitrary rewrites
PartialManaged publication is a separate boundary
PartialReplayable semantic evidence
PartialMulti-module projects and offline scaffolding
PartialInterpreter, native and Core Wasm execution
PartialBounded scalar JavaScript/TypeScript exports
PartialTyped runtime Agents
PartialOwnership and replayable cleanup
PartialA broader everyday language
PartialBudgets, durable recovery and model calls
ExperimentalApplication and economic-agent experiments
Developer previewGenerated boundaries remain profile-specific
RoadmapBroad native and application support
RoadmapGeneral bidirectional ecosystem interoperability
DemonstratedSigned release provenance
Developer previewCompiler-owned generic target boundary
Developer previewOpt-in native and Wasm Agent stages
ExperimentalBounded source yields and durable continuations
ExperimentalLocal signed Registry-v3 trust
DemonstratedPinned Lean proof and obligation gate
PartialSource laws and replayed proofs
Developer previewRich native Rust integration
Developer previewSame-thread Rust Futures
ExperimentalCompiler-connected development harness
Developer previewChecked development hot reload
PartialContext, token and task-cost accounting
PartialInstall without a checkout
ExperimentalExplain model and tool choices
PartialRoute between accepted turns
PartialMore precise repair guidance
PartialBounded command and data profiles
DemonstratedKeep adverse proof results visible
PartialHarden the harness boundaries
PartialStrict JSON and bounded ASCII patterns
Developer previewNative Project test gate remains pending

Current status	Source state	Evidence and provenance	Publication state	Supported scope	Evidence
Canonical source and stable identity `stable-semantic-program-graph`	Partial	Exact-tag Project and Rust jobs passed the admitted graph contracts; the full semantic-foundation goal remains Partial.	Bounded beta source/toolchain profile	Readable `.spx` remains the canonical Git representation. Explicit `@id` values identify declarations independently of supported display-name changes. The revision binds canonical source and the compiler-owned implicit prelude, not incidental source spans or a graph wire format.	GitHub repository
Bounded context and compact projections `bounded-agent-context`	Partial	Bounded typed context, compact replay and committed local tokenizer comparisons are implemented.	Bounded beta source/toolchain profile	Select exact graph or task context with depth, direction, node and byte bounds. Model-text v2 reduces tokens on selected large inputs and grows on small ones; reports preserve the tokenizer and comparison boundary.	GitHub repository
Semantic edits, not arbitrary rewrites `revision-bound-semantic-patches`	Partial	Exact-tag source-repair and Project jobs passed bounded edit contracts; arbitrary repository rewrites are outside scope.	Bounded beta source/toolchain profile	Inspect context, derive a candidate, preview impact, review, replay checks, then explicitly authorize application. The operation families now extend beyond renames to bounded expression replacement, structural changes and specified rebase/merge composition. Each protocol keeps its own revision, identity and operation limits.	GitHub repository
Managed publication is a separate boundary `managed-workspace-semantic-operations`	Partial	Project Product Acceptance passed on Linux, macOS and Windows; publication still requires explicit authority.	Bounded beta source/toolchain profile	Managed workspace generations, candidate evidence, Project revision storage and MCP workflows retain explicit write and publication authority. Validation of multiple files is not an atomic update to arbitrary raw paths, Git or editors. The Rust embedding API supplies capped inputs, cancellation and opaque sessions, not unrestricted host access.	GitHub repository
Replayable semantic evidence `semantic-evidence-capsules`	Partial	Revision-bound evidence is implemented and release claim reconciliation passed; a receipt grants no mutation authority.	Bounded beta source/toolchain profile	Evidence binds checked facts and candidate changes to source and revisions. A receipt can support review or rejection; it does not grant execution, mutation or publication authority.	GitHub repository
Multi-module projects and offline scaffolding `bounded-multi-file-project`	Partial	Project Manifest, Product Acceptance and installed-toolchain journey jobs passed; service-host breadth is separately scoped.	Bounded beta source/toolchain profile	Manifests define declared source, entries, tests and exports. Bundled calculator, library and service templates have their own profiles. new creates a fresh project from compiled-in files; source checking, interpreted tests and target builds follow the selected manifest contract.	GitHub repository
Interpreter, native and Core Wasm execution `native-and-wasm-lowering`	Partial	Five platform archives and selected native/Wasm gates passed; individual runtime profiles retain separate admission limits.	Bounded beta source/toolchain profile	Admitted scalar, owned-data, generic, collection and immutable-list profiles execute through interpreter, native C11/Clang and Core Wasm with profile-specific conformance. Opt-in Agent stage hosts are separately bound; ordinary yields still refuse native/Wasm emission.	GitHub repository
Bounded scalar JavaScript/TypeScript exports `public-wasm-scalar-exports`	Partial	The exact-tag Chromium scalar-export job passed; other browser engines and owned-data packages are separate.	Bounded beta source/toolchain profile	Stable-ID scalar exports have a separate public Wasm profile and browser fixture. Owned-data packages, broad browser support, components and generic signatures have their own contracts and cannot inherit this support claim.	GitHub repository
Typed runtime Agents `bounded-agent-runtime`	Partial	AGENT-06 lifecycle/client jobs passed across Linux, macOS and Windows. Default live routes remain interpreter-selected; opt-in held target hosts have separate bounded evidence.	Bounded beta source/toolchain profile	Typed source roles drive initialization, observation, model proposals, authorization, effects and reduction. Bound Proposal schemas constrain decoding. Default live routes use the interpreter; selected library routes can supply held native C11/Core Wasm stage hosts under their own local parity and recovery gates.	GitHub repository
Ownership and replayable cleanup `ownership-inspired-memory-management`	Partial	GEN-05B and Rust jobs passed admitted ownership profiles; general lifetime safety remains open.	Bounded beta source/toolchain profile	Owned and borrowed values, cleanup plans, selected records/variants and resource compositions are executable. Bounded owned Bytes, scalar-snapshot, transactional mutable and synchronous borrowed-text callbacks have move, escape and cleanup controls. General lifetimes, arbitrary capture shapes and public borrowed ABIs remain open.	GitHub repository
A broader everyday language `everyday-language-and-collections`	Partial	The exact-tag STD-08 bundled-library job passed; complete Everyday library and physical providers remain open.	Bounded beta source/toolchain profile	Records, variants, classes, inheritance, scoped generic inference, Option/Result, mutation, loops, vectors, iterators, function values and bounded closures support useful programs. Immutable List<i64> adds persistent constructors and source-bound law examples; broader constraints and feature combinations retain limits.	GitHub repository
Budgets, durable recovery and model calls `model-budgets-and-durable-recovery`	Partial	AGENT-06 jobs passed bounded lifecycle and accounting paths; provider bills and host policies remain external facts.	Bounded beta source/toolchain profile	Explicit host adapters supply credentials, transport and stores. Limits can cover calls, tokens, bytes, deadlines and quoted costs. Durable profiles acknowledge intent before dispatch and refuse uncertain redispatch. Generic host profiles support bounded retry/failover; the bound source-model route does not automatically retry or switch providers. Usage observations are not guaranteed invoices.	GitHub repository
Application and economic-agent experiments `application-and-economic-agent-profiles`	Experimental	The bounded reference snapshot host has local packaged and selected hosted Linux/Podman evidence; economic-agent authority remains explicitly supplied.	Bounded beta source/toolchain profile	Reference-service routes compose checked session, task and job decisions with snapshot persistence and selected JSON-event or OTLP telemetry. SQL adapters are refused. Economic Agents retain explicit wallet, simulation, approval, signing and reconciliation responsibilities; no external exactly-once guarantee follows.	GitHub repository
Generated boundaries remain profile-specific `owned-data-package-previews`	Developer preview	Project Product Acceptance and native Rust SDK jobs passed on three hosts; generated package publication remains undecided.	Generated/private preview; publication and public support are separate decisions	Project v8 carries Bytes and selected Option/Result forms; v9 adds flat owned records, v10 owned UTF-8 and v11 nested owned records. Generated native/Rust and npm/Wasm consumers, private transports and public generic metadata each have separate contracts. Toolchain release, package publication and public support are different decisions.	GitHub repository
Broad native and application support `broad-platform-support`	Roadmap	Five toolchain archives are published, and bounded browser/mobile/desktop profiles exist. A complete supported application platform across browser engines, physical devices, operating systems and installed workflows remains a broader product requirement.	Full support not established	Five toolchain archives are published, and bounded browser/mobile/desktop profiles exist. A complete supported application platform across browser engines, physical devices, operating systems and installed workflows remains a broader product requirement.	GitHub repository
General bidirectional ecosystem interoperability `bidirectional-ecosystem-interoperability`	Roadmap	General ownership-safe foreign interfaces, stable aggregate/resource/component and generic ABIs, maintained package publication and broad host-language compatibility remain open. Metadata, generated code and private host fixtures do not complete this requirement.	Full support not established	General ownership-safe foreign interfaces, stable aggregate/resource/component and generic ABIs, maintained package publication and broad host-language compatibility remain open. Metadata, generated code and private host fixtures do not complete this requirement.	GitHub repository
Signed release provenance `release-provenance`	Demonstrated	Published 11 October 2026 at 15:07 UTC. All 91 jobs in the exact-tag publication run succeeded. Five toolchain archives and two installers ship with SHA256SUMS, five archive attestations and independently verified signed aggregate provenance. Native installer journeys gate publication. Archives are not notarized or claimed reproducible; offline verification does not establish current revocation state.	Published beta toolchain and provenance assets	Five archives, two installers, checksums and five attestations are published. The publication job verifies signed aggregate provenance and exact candidate equality after native install journeys; this is no notarization or reproducible-build claim.	GitHub repository
Compiler-owned generic target boundary `public-generic-compiled-boundaries`	Developer preview	The exact-tag generic milestone passed on Linux, macOS and Windows; a private checked Core Wasm provider, TypeScript carrier and native settlement corpus execute.	Unpublished private profile; PG-9 remains unsupported	One admitted generic endpoint and bounded consumer/settlement cases are real. Wider endpoint shapes, public ABI support and package publication remain open.	GitHub repository
Opt-in native and Wasm Agent stages `source-agent-target-parity`	Developer preview	Bounded source Agent stages execute through sealed interpreter, native C11 and Core Wasm routes, with selected local parity, recovery and migration gates.	Explicit library target selectors; default live routes remain interpreter-selected	A host supplies the held native or Wasm runtime explicitly. This does not establish general instruction metering, unrestricted cleanup or finalizer parity, every source profile, or broad deployed/hosted Agent target support.	GitHub repository
Bounded source yields and durable continuations `bounded-resumable-effects`	Experimental	Interpreter profiles admit sequential and control-dependent yields, selected owned-Bytes carrying and authenticated durable source recovery. A public owned-Agent slice has two-turn and selected process-restart gates.	No public native/Wasm continuation ABI	Each profile bounds suspension sites, owned state and restoration phases. Ordinary native/Wasm emitters still refuse yielding functions. General scheduling, arbitrary owned continuations, universal migration and a stable public continuation ABI remain open.	GitHub repository
Local signed Registry-v3 trust `signed-registry-local-trust`	Experimental	Producer-backed roots and leaves, signed metadata, held generations, lock-bound artifact reads and cache bridging have focused local gates.	No hosted registry or public distribution	Signed local evidence grants no ambient fetch, execution or package-publication authority. Production roots, network transport and supported distribution remain separate.	GitHub repository
Pinned Lean proof and obligation gate `lean-kernel-obligation-gate`	Demonstrated	The exact-tag hosted Lean job passed the Kernel-0 proof, axiom audit, generated obligation export and differential corpus.	Bounded research proof, not a general safety certificate	The proof covers its formal Kernel-0 slice. It does not prove the full language, all backend behavior or absence of vulnerabilities.	GitHub repository
Source laws and replayed proofs `source-laws-and-proofs`	Partial	Native law syntax, selected law inventories, protected repair and bounded installed Lean/Z3 profiles have executable positive and mutation/refusal evidence.	Bounded source and proof-tool profiles	Contract, relational, modular scalar, finite structured, protocol and immutable-list laws keep exact source and proof identities. Unsupported goals remain open or refused; lowering, foreign internals and external side effects are outside a general proof claim.	GitHub repository
Rich native Rust integration `native-rust-rich-interop`	Developer preview	Selected imports, generated owners/views/callbacks and real Regex/Url, Serde/iterator and reqwest/Tokio application gates exist.	Generated developer previews; selected native signatures	Owner-tied views and bounded FnOnce, FnMutI64 and synchronous borrowed-text captures preserve their specific lifetime and rollback contracts. Application receipts include adverse throughput and guest-host limits; arbitrary crate, ABI and zero-overhead claims remain open.	GitHub repository
Same-thread Rust Futures `local-rust-futures`	Developer preview	Generated local Future handles, selected source yield, caller-owned executors and real HTTP/cancellation/shutdown controls have local evidence.	Bounded local generated and Project-selected profiles	The host supplies the executor and runtime. One admitted source suspension and exact Project revision are bound to the generated adapter; streams, cross-thread execution, durable arbitrary Future state and universal async imports remain separate.	GitHub repository
Compiler-connected development harness `compiler-assisted-harness`	Experimental	Task/plan/repair feedback, provider locks/trust, retrieval, official skills, model routing and bridge/MCP have local and selected hosted Linux evidence.	Full-toolchain harness and standalone host; explicit project setup	Project-selected Graft/Graphify, RTK views and Ponytail/Caveman skills support bounded workflows. WikiSkill evolution and routing qualification are explicit gates. Windows, broader model/platform results and automatic default changes require additional evidence.	GitHub repository
Checked development hot reload `checked-hot-reload`	Developer preview	Retained interpreter sessions and VS Code controls pass selected macOS arm64 activation, rejection, safe-point and lifecycle gates.	Bounded local dev session; source-Agent migration is a separate lane	Candidates are checked before activation and invalid edits leave the active revision usable. The recorded small fixture reload is slower than restart. Other operating systems, native/Wasm state swapping and production rollout remain outside this result.	GitHub repository
Context, token and task-cost accounting `task-token-accounting`	Partial	Exact local tokenizer reports, session aggregation and normalized provider receipts are implemented; the recorded paid campaign did not qualify a change to defaults.	Local measurement and explicit provider-accounting profiles	Keep comparable selected payloads, tokenizer fingerprints, reservations, observed usage and reported/estimated money separate. Missing usage remains unavailable and failed calls remain accounted for. The recorded best saving did not meet the declared threshold.	GitHub repository
Install without a checkout `verified-installers`	Partial	Per-user shell and PowerShell installers verify the selected archive and manifest, smoke the staged binary and activate atomically. Publisher verification is reported separately from checksums.	Scoped beta implementation; qualification remains profile-specific	Per-user shell and PowerShell installers verify the selected archive and manifest, smoke the staged binary and activate atomically. Publisher verification is reported separately from checksums.	GitHub repository
Explain model and tool choices `shared-model-routing`	Experimental	One decision core serves development and runtime routing. Rules are the default; adapters can recommend screened model profiles, tools or specialists. Recommendations never grant capabilities or replace authorization.	Scoped beta implementation; qualification remains profile-specific	One decision core serves development and runtime routing. Rules are the default; adapters can recommend screened model profiles, tools or specialists. Recommendations never grant capabilities or replace authorization.	GitHub repository
Route between accepted turns `durable-turn-routing`	Partial	Host-approved deployment profiles can change at durably accepted turn boundaries. Handoffs retain digests and bounded state; uncertain model or effect dispatch stops for reconciliation rather than switching models.	Scoped beta implementation; qualification remains profile-specific	Only an accepted settled turn can open a new route. A handoff carries at most 16 KiB state, accepted-output digests and result references, not the transcript. Delegation reserves the parent allowance and inherits its deadline. Tool/specialist choices are reauthorized against live grants and argument schemas; uncertainty halts for reconciliation.	GitHub repository
More precise repair guidance `agent-repair-guidance`	Partial	Diagnostics name exact imports, literal suffixes, ownership repairs and effect declarations. Installed language topics and the generated project AGENTS.md guide small edit-check steps. VS Code can select and probe the compiler.	Scoped beta implementation; qualification remains profile-specific	Diagnostics name exact imports, literal suffixes, ownership repairs and effect declarations. Installed language topics and the generated project AGENTS.md guide small edit-check steps. VS Code can select and probe the compiler.	GitHub repository
Bounded command and data profiles `native-command-resource-output`	Partial	The tagged source includes native-only Project v26/v28 commands, strict JSON scanning and bounded ASCII patterns. Each has its own admission and evidence; authored native tests still have a pending current-head gate.	Scoped beta implementation; qualification remains profile-specific	Project v26/v28 source-command routes are native-only. v28 admits 1 MiB per String and 1 MiB combined staged output with bounded append, while file reads and capabilities keep their older bounds. std.data.json.scan validates complete UTF-8 JSON with explicit duplicate-key policy; std.pattern is a bounded ASCII byte matcher. These additions do not widen every interpreter, Wasm or public API profile.	GitHub repository
Keep adverse proof results visible `law16-retained-campaigns`	Demonstrated	A separate LAW16 Claude campaign completed 20 trials for USD 0.291235: 19 passed independent candidate/attack replay, one Bend candidate failed. Nine matched pairs fully passed; this is no general language or cost ranking.	Scoped beta implementation; qualification remains profile-specific	A separate LAW16 Claude campaign completed 20 trials for USD 0.291235: 19 passed independent candidate/attack replay, one Bend candidate failed. Nine matched pairs fully passed; this is no general language or cost ranking.	GitHub repository
Harden the harness boundaries `harness-protocol-hardening`	Partial	Updates preserve revocations under concurrent writes; cancellation is terminal; bridge queues are bounded; idle protocol violations stay quarantined. Graft output fits the request budget and Graphify results remain request-scoped.	Scoped beta implementation; qualification remains profile-specific	Updates preserve revocations under concurrent writes; cancellation is terminal; bridge queues are bounded; idle protocol violations stay quarantined. Graft output fits the request budget and Graphify results remain request-scoped.	GitHub repository
Strict JSON and bounded ASCII patterns `strict-json-and-ascii-patterns`	Partial	Strict JSON scan has focused local interpreter/native/Core-Wasm and bundling checks; the pattern catalog records a bounded source package.	Additive source packages; no universal regex or JSON object API	std.data.json.scan validates a whole borrowed UTF-8 document with bounded depth and explicit decoded-key duplicate policy. std.pattern matches bounded ASCII bytes with flat captures and logical-work limits; general regular expressions and Unicode character semantics are outside scope.	GitHub repository
Native Project test gate remains pending `native-project-tests-pending`	Developer preview	The tagged specification marks the current-head executable gate pending. Authored source is not a passed current-head result.	Authored opt-in profile, not a support promotion	semaprax test <project> --target native selects authenticated v26/v28 test roots, with 10-second and 65,536-byte defaults per root. Compilation is outside that timeout. Ordinary interpreter behavior and native-only refusal remain unchanged; hosted or physical-device qualification is not claimed.	GitHub repository

Boundaries that remain open

Beta release evidence does not establish production readiness, universal memory safety or absence of bugs.
A successful workflow covers the gates it ran. Ignored tests, unprovisioned hosts and additional target combinations require separate evidence.
Native law proofs cover their selected semantics and assumptions. They do not prove arbitrary Rust internals, all lowering or external settlement.
Generated Rust/npm package publication, public generic ABI support and broader Project profile promotion remain separate decisions.
Default live Agent routes use the interpreter. Opt-in caller-held native/Wasm stage routes have bounded evidence, not unrestricted backend parity.
Model providers, credentials, stores, wallet signing and external authority remain explicitly configured host responsibilities.
Durable recovery preserves uncertainty; it does not guarantee exactly-once network/payment effects or provider billing.
Compact payload reductions and paid trials do not establish a general token, latency, quality or task-cost advantage.

// STATUS

Repository status at the audited snapshot

Repository snapshot	`933196b` · 2026-10-15. The v0.9.0 tag resolves to the pinned source commit. Its exact-tag CI completed successfully. This does not establish blanket production or security assurance.
Full product status	55 Partial · 0 Implemented · 0 Missing
Graph and project contract	Canonical source, stable IDs and checked compiler representations connect laws, semantic queries, edits and execution. Feature-selected graph and Project schemas preserve their own admission, compatibility and host-authority contracts.
Published beta release	`v0.9.0` · Published 11 October 2026 at 15:07 UTC. All 91 jobs in the exact-tag publication run succeeded. Five toolchain archives and two installers ship with SHA256SUMS, five archive attestations and independently verified signed aggregate provenance. Native installer journeys gate publication. Archives are not notarized or claimed reproducible; offline verification does not establish current revocation state. Exact-tag CI.
Package and API previews	The release includes useful language, law, harness and host-integration profiles. Generated Rust/npm packages, public generic ABIs and broader platform support retain separate publication and support decisions.

Reviewed on 15 October 2026 against the v0.9.0 commit, published assets and release run. The tagged install handbook and channel registry still show v0.8.0 examples; use this page’s pinned v0.9.0 downloads. Older matrix/roadmap headings are historical. The live handbook follows main and can describe newer work. GitHub repository.

// DOCS

Open the Semaprax handbook

The online handbook is the English guide published from main and may cover changes after 0.9.0. Use the pinned snapshot when reproducing this release.

Live handbook

The current English learning path, published from main.

0.9.0 handbook snapshot

The handbook files at the exact reviewed release commit.

Build your first project

Current English guide to the calculator manifest, checks, tests and builds.

Learn the language essentials

Current English introduction to values, functions and source structure.

Work with a coding agent

Current English guide to semantic context and safe change workflows.

CLI reference for 0.9.0

Pinned command forms and the standalone/full-toolchain boundary.

VS Code extension

Pinned setup, semantic navigation, review and development controls.

Runnable examples

Pinned examples for the language, projects, laws, Agents and host integrations.

// REF

Primary sources for this page

// FAQ

Questions and practical answers

What does Demonstrated mean?

A named artifact or execution path passed its dedicated gate under the stated source, host and feature constraints. The ledger also records Partial, Developer preview and Experimental profiles. A demonstrated slice does not establish complete language or platform support.

Does a green CI run prove security?

It supplies evidence for the checks that actually ran, including positive and adverse paths. Version 0.9.0 also has signed release provenance and archive attestations. Those checks do not prove absence of vulnerabilities, cover every ignored or provisioned test, or turn a bounded proof into whole-language correctness.

Research project by Wavect: Wavect GmbH. Created by Wavect as an open-source systems research project.