Stable identity first. Source edits second.
Stable identities connect checked source, semantic queries, proof obligations and proposed changes. In v0.9.0 a shared decision core also connects development and runtime model selection, while the host retains deployment authority. Native command, data and ownership additions remain explicitly selected profiles.
entity Semaprax
status beta
snapshot 933196b
authority github.com/wavect/semapraxSemaprax 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.
Pick a stage to highlight its parts of the architecture below.
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 a bounded formal kernel and obligation export. Release jobs separately attest five archives, verify the signed aggregate set and exercise each native installer journey before publication. These evidence chains do not prove full-language correctness, notarization or cross-host reproducibility.
Hard screening checks confidentiality, tools, modalities, context and budgets before an advisory router sees candidates. Development phases and runtime deployments share engine code but keep separate evidence keys. Rules make zero router calls; no learned adapter is live-tested or qualified in the dated support record.
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.
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.
Installed diagnostic topics suggest exact imports, effect declarations, ownership repairs and admitted syntax. Manifest formatting has an explicit fmt –manifest mode. Tagged optimization work preserves identity, HIR replay, loan accounting and resource ceilings; individual source receipts and pending gates remain visible rather than implying measured whole-project speedups.
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)
}| 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.
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.
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 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.
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.