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.``
