Laws beside the source
Declare stable laws, select the proof inventory and replay supported Lean/Z3 obligations. Repair implementation bodies while protecting the intended requirement.
EvidenceV0.8.0 BETA · APACHE-2.0
The systems language built for coding agents, and readable by humans.
Readable source. Queryable meaning. Checked changes.
Give coding agents the types, contracts and relationships behind your code. Semaprax 0.8.0 brings source laws and proof tools, richer Rust integration, a development harness, checked hot reload and task-level token reporting into one beta toolchain. Start with a small program, then connect the parts your project needs.
revision sha256:<program-state>
query app.main --depth 1
context typed · bounded · stable-id
patch expected_revision == current
verify fail_closed
target native | browser/wasm// STATUS
Repository status at the audited snapshot
| Repository snapshot | 615e501 · 2026-10-06. The v0.8.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.8.0 · Published 6 October 2026 at 07:37 UTC. All 82 exact-tag jobs succeeded. Three toolchain archives, SHA256SUMS, per-archive attestations and signed aggregate provenance were published. The release job independently verified the signed set before publication. The 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. |
What 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.8.0 also includes typed runtime Agents, a compiler-connected development harness and bounded Rust, native and WebAssembly integrations.
// v0.8.0
What changed in v0.8.0
Six practical advances in the 0.8.0 source and published beta toolchain.
Richer Rust integration
Selected Rust APIs, generated owner and callback adapters, and real Regex/Url, Serde/iterator and Tokio/reqwest applications extend the bridge beyond scalar demos.
EvidenceA compiler-connected harness
Combine semantic context with project-selected providers, Graft/Graphify, RTK views, official Ponytail/Caveman skills and explicit model-routing policies.
EvidenceChecked development reload
The dev command and VS Code controls validate candidates, wait for a safe activation boundary and retain the active program after an invalid edit.
EvidenceToken and task-cost reports
Compare exact context payloads, inspect session regressions and reductions, and distinguish provider receipts from reservations and estimated cost.
EvidenceA verified release asset set
All 82 exact-tag jobs passed. Three prebuilt archives ship with checksums, build attestations and independently verified signed provenance.
Evidence// v0.8.0
Prefer a prebuilt command-line tool?
Version 0.8.0 publishes archives for Apple Silicon macOS, Linux x86-64 GNU and Windows x86-64 MSVC. There is no graphical installer in this release. Each archive includes the full toolchain under the name semaprax, plus semapraxd and a smoke example. Source installation keeps the full build separately named semaprax-full.
macOS · Apple Silicon
aarch64-apple-darwin
Linux · x86-64 (GNU)
x86_64-unknown-linux-gnu
Windows · x86-64 (MSVC)
x86_64-pc-windows-msvc
- Choose the archive that matches your operating system and CPU. The GitHub Source code downloads are repository snapshots, not prebuilt executables.
- Check SHA256SUMS before extracting your platform archive. Add its extracted directory to PATH or invoke semaprax by its full path.
- Run
semaprax --version, then check and run the includedsmoke/meaning.spxfrom the extracted directory. It returns 42. Clang is needed for native builds; the web examples use Node.js 22+. - For signed provenance verification, collect all three archives and the signed metadata in one directory, then follow the linked instructions for
semaprax release verify <release-dir>. Require the cryptographically verified offline result; a successful unsigned verification does not validate a signature.
SHA256SUMS · Checksums and signed provenance · Release manifest · Release record
// CLI
Run your first checked program
Source route, pinned to the reviewed commit. Requires Git and Rust/Cargo 1.88+. The first Cargo run may fetch dependencies. These check/run commands need neither Clang, Node.js nor an AI provider; the program returns 42.
git clone https://github.com/wavect/semaprax.git
cd semaprax
git checkout --detach 615e501612895a52b3fdd72a03baf875a8f0df1b
cargo run --locked -p semaprax -- check examples/meaning.spx
cargo run --locked -p semaprax -- run examples/meaning.spx// PROJECT
Install once, then create a project
Continue in the same pinned repository checkout. Cargo installs the standalone CLI; the PATH line below applies to Bash and Zsh. The generated calculator includes source, a manifest, tests and AGENTS.md. Choose a fresh destination; new uses bundled files and does not initialize Git or contact a package registry.
cargo install --locked --path . --bin semaprax
export PATH="$HOME/.cargo/bin:$PATH"
semaprax --version
semaprax new first-semaprax
semaprax check first-semaprax/semaprax.toml
semaprax test first-semaprax/semaprax.toml
semaprax run first-semaprax/semaprax.toml// AGENT
Give your coding agent a precise starting point
From the repository root, inspect the same program by stable identity. Graph, context and installed language help are read-only starting points. A later semantic edit needs its current revision, supported operation and explicit application step.
semaprax graph examples/meaning.spx
semaprax context examples/meaning.spx app.main --depth 1 --max-bytes 65536 --max-nodes 256
semaprax context examples/meaning.spx math.add --depth 1 --filters contracts
semaprax help language
semaprax help diagnostic SPX-T208// 01
One 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.
// 02
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
// 03
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.
architecture
Architecture
Source laws, semantic graphs, Agents and harness
evidenceEvidence
What v0.8.0 implements and where it stops
benchmarksBenchmarks
Measured tokens, task cost and performance
interoperabilityInteroperability
Target and ecosystem evidence matrix
roadmapRoadmap
Milestones, objectives, and open gaps
// 04
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.8.0. Use the pinned snapshot when reproducing this release.
Live handbook
The current English learning path, published from main.
0.8.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.8.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 against the v0.8.0 tag and its pinned source commit. Versioned specifications define admission and authority; older release headings in the matrix and roadmap are historical.
- v0.8.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
// FAQ
Questions and practical answers
Is Semaprax production-ready?
Version 0.8.0 is an Apache-2.0 beta released on 6 October 2026. You can install it, run programs and explore the implemented profiles. A successful exact-tag release does not establish production support; the full-goal matrix still records 55 Partial requirements.
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 against the v0.8.0 tag and its pinned source commit. Versioned specifications define admission and authority; older release headings in the matrix and roadmap are historical.