Stable identity first. Source edits second.
The semantic program graph makes declarations, types, effects, contracts, ownership and call relationships queryable by stable identity. Version 0.8.0 extends that model into source laws, protected implementation repair, richer Rust boundaries and a development harness.
entity Semaprax
status beta
snapshot 615e501
authority github.com/wavect/semaprax| 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. |
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.
Readable .spx remains the canonical Git representation. An explicit @id identifies a declaration through supported display-name changes. Compiler-derived revisions bind source and the selected prelude; graph encodings expose those facts without replacing the source.
Select a declaration, direction, depth, node count and byte limit. Task context and text, binary or model-text projections preserve exact replay against the selected facts. The native semantic context broker can use Graft or Graphify for additional repository navigation without treating an external index as compiler truth.
Native law declarations give persistent identities to contract and relational requirements. A separately selected LawSet fixes the complete inventory and strict policy. Installed Lean/Z3 adapters prove admitted scalar, modular, structured and list laws; stale, unsupported, unknown and disproved results remain distinct. Candidate repair must satisfy the preserved requirement.
Inspect context, derive a candidate, preview impact and review, replay checks, then authorize application. Bounded expression replacement, structural edits and specified composition each retain their operation and revision limits. Source law edits and implementation repairs follow separate protection rules.
Managed workspace generations, candidate evidence and Project revision stores bind publication to the checked candidate. The Rust embedding API offers bounded inputs and opaque sessions. Multi-file validation alone does not update arbitrary files, Git refs or editor buffers.
Admitted profiles include records, variants, classes, inheritance, generics with scoped argument inference, Option/Result, loops, iterators, function values, strings and bytes. Immutable List<i64> adds persistent nil/cons/uncons operations. General constraints and arbitrary combinations still require their own admission.
Owned values, borrowed views, cleanup plans and selected resource compositions are executable. Narrow closure profiles include owned Bytes captures, copied scalar snapshots, transactional mutable scalar state and synchronous borrowed-text captures. Each checks its own escape, move, rollback and cleanup rules; broader lifetime relations remain open.
Prepared Rust API indexes select supported imports and exact Cargo inputs. Generated owner, borrowed-view and callback adapters connect checked source to real Regex/Url and Serde/iterator consumers. A same-thread Future bridge uses a caller-owned executor. Foreign assumptions remain explicit; generated glue does not prove a crate’s internals.
Initialize, observe, propose, decode, authorize, execute and reduce. Authorization repeats each turn and the reducer chooses Continue, Complete, Suspend or Fail. Default live routes use the interpreter; opt-in library routes accept caller-held native C11 or Core Wasm stage hosts with bounded local parity evidence.
Explicit adapters supply transport, credentials and stores. Durable profiles acknowledge intent before dispatch and preserve unresolved attempts as uncertainty. Limits and receipts separate calls, work, bytes, tokens and costs. Generic host retries/failover and the bound source-model route have different contracts; the latter does not automatically switch providers or retry uncertain work.
The interpreter has bounded sequential and control-dependent yields, selected owned-Bytes carrying and authenticated durable source profiles. The public owned-Agent slice has a two-turn lifecycle and selected process-restart gates. Ordinary native/Wasm emitters still refuse yielding functions; a general scheduler and universal continuation ABI remain open.
The full toolchain’s harness coordinates explicit tasks, compiler feedback, provider descriptors, per-project locks and trust, model routing, skills and bridges. Official Ponytail/Caveman bundles, Graft/Graphify adapters and RTK model views serve selected workflows. Authoritative command results remain separate from compact model-facing output.
A retained interpreter session admits a candidate, plans compatibility and activates it between invocations. Polling watches declared Project inputs; invalid changes leave the active revision usable. VS Code controls expose active, pending and dirty state. Source-Agent journal migration is a separate full-toolchain lane.
A reference service composes checked session, task and job decisions with a snapshot host, explicit HTTP/TLS and selected JSON-event or OTLP telemetry. The accepted Linux/Podman journey remains bounded; SQL adapters are refused. Economic Agents retain host-owned wallet, approval, signing and reconciliation boundaries.
Owned-data Project profiles and a private compiler-owned generic Wasm endpoint have generated consumer evidence. Public generic support remains unsupported and unpublished. Local signed registry metadata, held generations and lock-bound reads do not themselves provide a hosted package registry or network-fetch authority.
The exact-tag Lean job checks its bounded formal kernel and obligation export. Release jobs separately attest the three archives and sign and verify aggregate provenance. These are distinct evidence chains; neither establishes full-language correctness, notarization or cross-host reproducible builds.
module examples.meaning;
@id("math.add")
fn add(left: i64, right: i64) -> i64
requires left >= 0
requires right >= 0
ensures result == left + right
{
left + right
}
@id("app.main")
fn main() -> i64
ensures result == 42
{
add(19, 23)
}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. GitHub repository.
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.
The current English learning path, published from main.
The handbook files at the exact reviewed release commit.
Current English guide to the calculator manifest, checks, tests and builds.
Current English introduction to values, functions and source structure.
Current English guide to semantic context and safe change workflows.
Pinned command forms and the standalone/full-toolchain boundary.
Pinned setup, semantic navigation, review and development controls.
Pinned examples for the language, projects, laws, Agents and host integrations.
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.
The core graph is derived by the compiler from checked source, with stable declarations, types, contracts and relationships. The development harness can additionally use Graft or Graphify for repository navigation. Those external indexes complement the compiler’s semantic facts and do not replace its revision and validation rules.
The toolchain exposes specific revision-bound edit operations, candidate review and replay checks. Protected law inventories keep requirements separate from editable implementation bodies. An agent must use an admitted operation and authorized application route; a context query or successful proof is not permission to overwrite arbitrary files.