DEV Community: Kevin Riedl

What a semantic patch can honestly prove about WebAssembly output

Kevin Riedl — Mon, 24 Aug 2026 21:19:22 +0000

When a coding agent changes a systems program, a source diff is only the beginning of the question.

The more useful question is: what exact machine-facing artifacts would this semantic change produce, and can another process independently verify that relationship?

That is one of the research problems we are exploring in SEMAPRAX, an Apache-2.0 agent-native systems programming language built at Wavect GmbH.

SEMAPRAX is currently v0.2 pre-alpha experimental research software. It is not production-ready. The narrow mechanism described here is useful precisely because its claims are bounded.

From a patch to target projections

SEMAPRAX has a read-only command:

semaprax target-evidence <file> <patch.spatch>

The command takes a verified source snapshot and a semantic patch. It independently rebuilds both the base program and the patched candidate, then derives several deterministic compiler-owned projections:

semantic Graph JSON
an explicit capability manifest
Native C11 source
a structurally validated WebAssembly Core module

For every projection, the report records a domain-separated digest and byte length. It also classifies the projection as changed or unchanged.

That sounds simple, but the distinction matters. A source edit can leave one projection unchanged while altering another. A documentation-level identity change, a capability change, and a runtime-behavior change should not all be flattened into the same “some bytes changed” signal.

The target report therefore binds the proposed semantic change to the compiler artifacts it actually affects.

Why deterministic output is the prerequisite

Evidence over compiler output is only useful when the output is reproducible.

SEMAPRAX treats source formatting, semantic graph data, diagnostics, semantic patches, and target artifacts as deterministic projections. The same admitted input must produce the same bytes. Otherwise a digest says little: a second verifier could not distinguish a meaningful change from nondeterministic code generation.

This is also why the report uses domain separation. A digest of a semantic graph should not be confused with a digest of a Wasm module, even if a contrived byte sequence happened to match. Each artifact is hashed in its own named domain.

The WebAssembly boundary

The current WebAssembly lane uses the profile semaprax.wasm-core.v1. The emitted module is structurally checked using wasmparser 0.256.0 with its full feature set.

Structural validation answers a real but limited question: is this byte sequence a structurally valid WebAssembly Core module under that validator configuration?

It does not answer whether the program was executed correctly. It does not establish host compatibility, ABI correctness, safety, performance, provenance, policy approval, or conformance across runtimes.

SEMAPRAX’s public Wasm support is deliberately partial today. It covers bounded scalar exports and generated JavaScript/TypeScript bindings. It is not general WASI support, and it is not a broad WebAssembly Component Model implementation.

Those nonclaims are part of the design. Evidence becomes dangerous when a convenient static fact is presented as a stronger runtime guarantee.

Replay before authority

A target report is still only evidence. By itself, it has no permission to modify source.

SEMAPRAX can wrap the report in an additive Evidence v2 capsule tied to the semantic patch. The evidence-gated apply route acquires the ordinary single-file authority, independently replays the exact bounded change, reconstructs the target report, and checks the binding before committing.

Conceptually, the route is:

verified source snapshot
        +
semantic patch bytes
        |
        v
independent replay
        |
        +--> candidate semantic graph
        +--> candidate capability manifest
        +--> candidate Native C11 source
        +--> candidate Wasm Core module
        |
        v
exact evidence comparison
        |
        v
commit or fail closed

If the source snapshot drifted, the patch bytes differ, replay fails, or any bound artifact differs, the evidence-gated route must not commit the change.

This keeps three ideas separate:

Meaning — the verified semantic change.
Evidence — deterministic facts about its projections.
Authority — the narrow operation allowed to publish it.

Why this may matter for agent-written systems code

Text diffs are optimized for human review. Agents can consume them too, but they do not directly expose persistent semantic identity, resolved relationships, capability changes, or target consequences.

An agent-oriented toolchain can make those facts first-class without pretending that agents are infallible. The goal is not to replace review with a digest. The goal is to give reviewers and automated policies a replayable statement that is narrower, more precise, and easier to falsify.

For WebAssembly toolchains, this raises practical questions we would value feedback on:

Which compiler facts are useful to bind alongside Wasm bytes?
Which runtime observations belong in a separate evidence layer?
How should toolchains describe validator configuration so reports remain replayable years later?
Where should the boundary sit between a compiler-owned artifact and host-owned execution evidence?

You can inspect the research project at wavect.io/semaprax and the SEMAPRAX source repository.

Disclosure: coding agents have been used extensively as development assistants on SEMAPRAX. Wavect GmbH retains human responsibility for the project and uses executable quality gates. The implementation remains experimental and not production-ready.``

Why Agent Edits Need Semantic Identity: Building SEMAPRAX in Rust

Kevin Riedl — Sun, 23 Aug 2026 12:56:48 +0000

Originally published on Wavect.

TL;DR: Text positions are fragile edit targets because formatting and nearby changes move them. SEMAPRAX instead gives declarations persistent identities, resolves source into checked HIR, projects deterministic graph views and binds patches to a revision. Rust newtypes keep declaration and expression identities distinct, while ordered collections and independent evidence replay make the boundary reproducible. This is a pre-alpha research design, not a claim of production readiness or complete language safety.

A coding agent should edit a declaration by identity and expected meaning, not by a line number that may already be stale. In SEMAPRAX, persistent declaration IDs survive ordinary source movement, checked HIR centralizes resolved meaning, and revision-bound patches fail closed when their source snapshot changes. Rust makes these distinctions explicit in the compiler's types.

This article explains that design as implemented in the pre-alpha research compiler. It is useful even if you never adopt the language: the same boundaries apply to refactoring engines, compiler services and agent tools that must turn an intention into a reviewable change.

Why are line and byte offsets poor agent edit targets?

A text edit usually says “replace bytes 418 to 463.” That address describes one file snapshot, not the program entity the agent meant. A formatter, comment or concurrent edit can move it. A name is better, but overloads, scopes and renames make names contextual too.

The SEMAPRAX language contract therefore makes human-readable .spx source the canonical Git projection while exposing a versioned semantic graph as the preferred agent interface. Public declarations carry persistent @id identities. Expression identities remain revision-scoped because preserving every transient syntax node across arbitrary rewrites would imply a stronger identity guarantee than the compiler can honestly provide. The distinction is part of the SEMAPRAX language and compiler contract.

How does Rust encode the identity boundary?

The HIR does not pass raw strings everywhere. It defines separate newtypes for declarations and expressions:

pub struct DeclarationId(String);
pub struct ExpressionId(String);

pub struct ResolvedFunction {
    pub id: DeclarationId,
    // checked signature, body and effects
}

This shortened example reflects the types in src/hir.rs at the audited revision. The benefit is mundane and important: a function that expects a persistent declaration target cannot accidentally receive an expression address. The compiler must perform an explicit conversion or reject the operation.

The same module stores declaration indexes in BTreeMap and relation sets in BTreeSet. Ordered collections are not sufficient for determinism, but they remove one common source of output drift: randomized hash iteration. Semantic order still has to be preserved where order affects execution.

Why resolve once into checked HIR?

If a graph exporter, native backend and Wasm backend each reconstruct meaning from syntax, they can disagree about types, ownership or call targets. SEMAPRAX resolves and verifies first, then downstream projections consume the checked representation. The published architecture and trust-boundary document describes this pipeline and separates implemented lanes from future authority.

That gives an agent a useful chain of custody:

Parse human-readable source.
Resolve names and persistent identities into HIR.
Verify types, effects, ownership rules and contracts admitted by the current language subset.
Project deterministic graph JSON or target artifacts from checked semantics.
Bind proposed changes to the source revision and expected semantic target.

The graph is therefore a compiler projection, not a second source of truth. Git still reviews source. The agent gains structured context without asking humans to review an opaque database.

What makes a semantic graph deterministic?

Determinism is a whole-pipeline property. Stable node identifiers do not help if edge order changes between runs or diagnostics depend on hash iteration. SEMAPRAX uses ordered indexes, explicit serialization, bounded traversal and canonical output rules in its Rust graph projection.

There is also a subtle prohibition: never “fix” execution vectors by sorting them for prettier JSON. Evaluation and cleanup order are semantic. Canonical sorting belongs only on mathematically unordered sets. Sequence-bearing data must retain the compiler-defined order.

How can evidence constrain an agent patch?

A serialized evidence capsule should describe why a patch is admissible, but possession of that capsule must not grant write authority. SEMAPRAX separates proof data from the component that owns the commit. Its patch route acquires the normal lock, independently replays the exact bounded evidence, checks the current source snapshot, and only then stages and commits the candidate. The patch-evidence implementation keeps replay and application visibly separate.

This design addresses three distinct failures:

Stale intent: the patch was valid for an older source revision.
Wrong target: the text still matches, but it now refers to a different declaration.
Forged confidence: a caller presents a plausible report without reproducing the checks.

Independent replay does not prove that a requested feature is wise. It proves a narrower and testable statement: this bounded proposal still satisfies the compiler checks to which its evidence is bound.

What should Rust compiler and agent-tool authors copy?

Use domain newtypes. Separate persistent entity IDs, revision-local node IDs, digests and capabilities at the type level.
Keep one checked semantic core. Make graph views and backends consume resolved meaning instead of reparsing names independently.
Design determinism deliberately. Specify ordering, serialization, diagnostics and failure behavior, then test repeat runs byte for byte.
Bind edits to snapshots. A semantic target without a source digest is still vulnerable to drift.
Keep evidence powerless. Replay evidence inside the authority boundary before staging any change.
Publish the limits. A completion matrix is more useful than a broad “implemented” label when different compiler lanes have different evidence.

SEMAPRAX follows the last rule with an evidence-gated completion matrix. It prevents a passing unit test for one projection from becoming a claim about every target or runtime.

What does SEMAPRAX not prove yet?

SEMAPRAX v0.2 is experimental pre-alpha research. Its current repository documents bounded native C11/Clang and WebAssembly Core lanes, deterministic semantic tooling and a growing verified subset. It does not claim production readiness, complete memory safety, all operating systems, a complete ownership system, full ecosystem interoperability, a public Component Model runtime or live economic authority.

The practical way to evaluate it is to inspect the source and dated evidence, not extrapolate from the project goal. Start with the SEMAPRAX architecture overview, then compare the public claims with the pinned compiler revision below.

How can you reproduce this walkthrough?

git clone https://github.com/wavect/semaprax.git
cd semaprax
git checkout ca339feffcadf77a679abe2f159376287cf2e22c
cargo run -- graph examples/hello.spx

The command inspects the graph projection at the exact revision used for this article. Run the repository's documented quality gates before treating any local modification as evidence.

Editorial disclosure: OpenAI Codex assisted with drafting and translation. The technical claims and code references were checked against SEMAPRAX commit ca339fe by Wavect. The article contains no performance or safety claim inferred from model output.

Final thoughts

Reliable agent editing starts by naming the thing that should change, the revision in which it exists and the checks that must still hold. Rust can encode those distinctions directly: persistent declaration identity is not an expression address, checked HIR is not raw syntax, and evidence is not authority.

SEMAPRAX is an experimental implementation of that boundary. Its useful lesson today is smaller than its long-term language goal: give agents semantic handles, make every projection deterministic, and fail closed when meaning or source state has moved.