Install without a checkout
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.
EvidenceV0.9.0 BETA · APACHE-2.0
The systems language built for coding agents, and readable by humans.
Readable source. Queryable meaning. Checked changes.
Install the beta without a source checkout, create a checked project and give coding agents precise compiler feedback. Semaprax 0.9.0 adds five native downloads, policy-first model and tool routing, and clearer repair guidance. Source laws, explicit ownership and revision-bound changes keep each proposed edit tied to the program you inspected.
revision sha256:<program-state>
query app.main --depth 1
context typed · bounded · stable-id
patch expected_revision == current
verify fail_closed
target native | browser/wasmWhat is Semaprax?
Semaprax is an open-source, agent-native systems programming language in beta. Readable .spx source stays in Git while coding agents query typed program meaning, check source laws and propose revision-bound changes. Version 0.9.0 adds prebuilt installers, policy-first model routing and clearer repair guidance around its typed runtime Agents, compiler-connected harness and bounded native, Rust and WebAssembly profiles.
// v0.9.0
What changed in v0.9.0
Eight changes to installation, routing, repair and retained evidence. Tagged source additions keep their own verification limits.
Five native downloads
Linux arm64 and Intel macOS join the existing targets. Linux requires glibc 2.35+; macOS and Windows minima are listed per archive. Each target passes its own installed-distribution journey before publication.
EvidenceExplain model and tool choices
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.
EvidenceRoute between accepted turns
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.
EvidenceMore precise repair guidance
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.
EvidenceBounded command and data profiles
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.
EvidenceKeep adverse proof results visible
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.
EvidenceHarden the harness boundaries
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.
Evidence// v0.9.0
Choose your v0.9.0 archive
Five full-toolchain archives: GNU/Linux x86-64 and arm64 (glibc 2.35+), Apple Silicon macOS 11+, Intel macOS 10.12+, and Windows x64 10 1809+ / Server 2019+. musl/Alpine and Windows ARM have no archive. Each includes semaprax and semapraxd. The published manifest is authoritative; the tagged handbook’s older download table is historical.
macOS · Apple Silicon · 11+
aarch64-apple-darwin
Linux · arm64 · glibc 2.35+
aarch64-unknown-linux-gnu
macOS · Intel · 10.12+
x86_64-apple-darwin
Windows · x64 · 10 1809+ / Server 2019+
x86_64-pc-windows-msvc
Linux · x86-64 · glibc 2.35+
x86_64-unknown-linux-gnu
- Download your platform archive and select its exact line in SHA256SUMS. GitHub Source code downloads are repository snapshots, not runnable programs.
- For publisher verification use gh attestation verify with the matching
release-attestation-<target>.json, repository wavect/semaprax and exact tag. A checksum alone is not a signature. - Extract to a permanent directory and add it to PATH, then run the first-project commands below. For receipt-managed upgrade, downgrade or uninstall, use the installer contract; do not mix package-manager ownership.
- Homebrew:
brew install wavect/tap/semapraxinstalls v0.9.0 on Apple Silicon and Intel macOS. The tap formula and successful post-release channel run were reviewed on 15 October. WinGet submission #447495 is still open; no published WinGet installation is claimed. The tagged handbook’s v0.8.0 examples are historical. Source builders should check out commit 933196b9ef3cb611343f1401e9eb0b08fa404d0a and distinguish the standalone package from semaprax-toolchain.
SHA256SUMS · Checksums and signed provenance · Release manifest · Release record
Install the full toolchain: macOS and GNU/Linux
Pinned v0.9.0 per-user installer. No Rust, Cargo, checkout or model account is required. It selects one archive, checks its checksum and manifest, smoke-tests it and records activation in a receipt. With GitHub CLI available it also verifies the publisher attestation; without it the receipt explicitly says checksum-only. Add --require-publisher-verification to refuse that fallback. Open a new terminal after installation.
curl -fsSL https://github.com/wavect/semaprax/releases/download/v0.9.0/install.sh | sh -s -- --version v0.9.0Windows PowerShell, then your first project
On Windows use the pinned command below with PowerShell 5.1 or 7, then open a new terminal. On macOS/Linux continue with the semaprax commands after the shell installer. Pick a destination that does not exist. The bundled calculator includes source, manifest, tests and AGENTS.md; its final run prints 42. Clang is needed only when you select native compilation.
powershell -ExecutionPolicy Bypass -c "& ([scriptblock]::Create((irm https://github.com/wavect/semaprax/releases/download/v0.9.0/install.ps1))) -Version v0.9.0"
semaprax --version
semaprax new first-semaprax
semaprax check first-semaprax/semaprax.toml
semaprax test first-semaprax/semaprax.toml
semaprax run first-semaprax/semaprax.tomlGive your coding agent a precise starting point
Inside the generated first-semaprax directory, start with its AGENTS.md and a focused language topic. Read small source files directly; use bounded semantic context for a precise question and inspect truncation. The full graph can be much larger than the source. The optional development harness and a source-defined runtime Agent are different surfaces.
cd first-semaprax
semaprax help language lists
semaprax query --capabilities
semaprax check .
semaprax test .
semaprax help diagnostic SPX-T208One program, three connected surfaces
People edit readable source, tools query checked meaning, and supported targets execute the admitted program. Each target and integration states which language features it accepts.
- Readable sourceCanonical .spx files, stable declaration IDs, contracts, laws and explicit ownership. Ordinary check and run commands need no model account.
- Checked meaning for toolsCompiler-derived context, impact, candidate review and proof obligations. The harness can add selected retrieval, skills and model providers around that semantic core.
- Controlled executionInterpreter, admitted C11/Clang and Core Wasm profiles, plus typed runtime Agents whose model proposals pass deterministic authorization before effects.
Semaprax semantic program graph: Semaprax checks readable .spx source and resolves it into HIR, its typed compiler representation. Source and semantic identities bind queries, law obligations, candidate changes and execution to the program that was inspected. Coding agents can use the harness around this core; runtime Agents separately decode proposals, authorize effects and reduce state under explicitly supplied host capabilities.
Make every proposed change easier to check
Stable identities let an agent target a declaration. Bounded context explains its role. Contracts and separately selected laws constrain the implementation, while candidate review and replay check the change before application. The harness records actual usage and task outcomes so efficiency claims can be tested against evidence.
MEASURE THE OUTCOME
Less repair ambiguity, with task cost and correctness checked separately
Follow the question you need to answer
Use the handbook for practical steps, architecture for the programming model, evidence for implemented profiles, benchmarks for measurements and interoperability for the boundary with your existing stack.
// 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. |
Capability evidence ledger
| Current status | Evidence state | Scope | Evidence |
|---|---|---|---|
| Canonical source and stable identity | Partial | 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 | Partial | 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 | Partial | 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 | Partial | 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 | Partial | 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 | Partial | 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 |
// 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
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.
- v0.9.0 release and platform downloads
- Exact-tag CI and release evidence
- Handbook snapshot for the reviewed source
- Source law declarations
- Rich native Rust integration
- Development harness providers and model receipts
- Checked hot-reload workflow
- Token reporting and checked-work reuse
- Full-goal completion matrix and remaining boundaries
- Signed provenance and independent verification
- Tagged changelog and release history
- Installer verification and platform baselines
- Homebrew formula: both v0.9.0 macOS archives
- Post-release channel verification run
- WinGet submission: still open at review
// FAQ
Questions and practical answers
Is Semaprax production-ready?
Version 0.9.0 is an Apache-2.0 beta published on 11 October 2026. All 91 jobs in its publication run passed and five archives are available. The full-goal matrix remains 55 Partial requirements; release success is not blanket production assurance.
Is Semaprax only for AI agents?
You can write, check and run ordinary .spx programs without an AI model or account. Coding agents use semantic context and supported changes through the tooling; source-defined runtime Agents are a separate typed programming abstraction. The English handbook walks through both.
Need this level of evidence-first engineering in your AI product?
See Wavect’s AI engineering work.Created by Wavect as an open-source systems research project. GitHub repository. 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.