Verifiable Compute Specification

Draft 0.1 | January 2026

Introduction

This specification defines Verifiable Compute, a layered extension to WebAssembly for two-party verifiable computation. It specifies how a WebAssembly module is invoked, receives inputs, and produces outputs in a setting where two parties jointly evaluate a program with assurances about the result.

Scope

This specification covers:

• A two-party computation model
• Value visibility at the input and output boundaries
• Taint propagation through instructions, linear memory, and globals
• The embedding interface: how functions are invoked with visibility-tagged arguments, how memory is read and written, and how results are returned
• The requirements for a conforming guest module

This specification does not cover:

• N-party protocols (n > 2)
• Specific implementation strategies — this specification defines the embedder interface, not how it is realized
• Standard host function interfaces — these are defined at a separate layer

Relationship to WebAssembly

This specification is designed as a layered extension to WebAssembly:

┌────────────────────┐
│ Verifiable Compute │ ← This specification
├────────────────────┤
│ WebAssembly Core   │ ← W3C WebAssembly Spec
└────────────────────┘

For rationale on why WebAssembly is a suitable foundation, see this explainer.

Conventions

The key words "MUST", "MUST NOT", "SHOULD", "SHOULD NOT", and "MAY" in this document are to be interpreted as described in RFC 2119.

Concepts

The verifiable compute model is structured around the following concepts.

Guest

A guest is the WebAssembly module being executed. A conforming guest is a standard WebAssembly module. No special annotations or modifications are required.

Embedder

An embedder is the host environment that loads, validates, and instantiates the guest with verifiable compute semantics. Each party runs an embedder instance, and the two instances cooperate to jointly execute the guest.

Conforming Embedder

A conforming embedder is an embedder that implements the semantics defined by this specification for all WebAssembly core instructions it supports.

Parties

A verifiable computation involves exactly two parties: the local party and the remote party. Each party runs an instance of the embedder. The two instances jointly execute the guest. The parties are distinguished by which inputs they provide and their perspective on visibility.

Visibility

Each value has a visibility that determines which parties can observe it. There are three visibilities: public, private, and blind. A public value is known to both parties. A private value is known only to the local party. A blind value is known only to the remote party. This distinction is symmetric: what is private to one party is blind to the other.

Taint

Every value in the VM has a taint: either concrete or symbolic. Taint determines whether the VM has access to the value's bit pattern. Taint propagates through instructions, memory operations, and globals.

Concrete

A concrete value is a value for which the VM has a definite bit pattern. Public values at the invocation boundary enter execution as concrete values.

Symbolic

A symbolic value is a value that is not concrete. The VM operates on symbolic values without access to their bit patterns. Private and blind values at the invocation boundary both enter execution as symbolic values — the VM does not distinguish between them.

Store

The verifiable compute store extends the WebAssembly store with a mapping from each value-carrying location to a taint (concrete or symbolic). The locations subject to taint tracking are linear memory bytes, global values, and local variables. This mapping is not observable by the guest.

Two-Party Model

Both parties MUST use the same guest module. Module identity is determined by the module's binary representation.

Both parties MUST agree on every state update during execution. Visibility determines which values each party can observe, not which operations they participate in.

Both parties MUST agree on the call configuration (see Invocation). The mechanism for reaching this agreement is outside the scope of this specification.

Note

Two common instantiations of this model are:

• One party provides private inputs. The other party can verify the result without learning those inputs.
• Both parties contribute private inputs and both learn the output, without either party learning the other's private inputs.

Values

At the invocation boundary, each input value has one of three visibilities:

• Public — known to both parties.
• Private — known only to the local party. The embedder MUST NOT reveal the value to the remote party.
• Blind — known only to the remote party. The embedder MUST NOT reveal the value to the local party.

During execution, public values are concrete and private and blind values are both symbolic.

Note

Concrete and symbolic describe the VM's view, not any individual party's view. An implementation may internally have access to the bit patterns of symbolic values — for example, a zero-knowledge prover knows its own witness concretely — but the VM does not. In zero-knowledge terminology, public inputs correspond to the instance and private inputs correspond to the witness.

Instructions

This section defines how taint propagates through WebAssembly instructions during execution.

Default Rule

An instruction produces a concrete result if all of its operands are concrete. Otherwise, the result is symbolic.

Annihilator Exceptions

A binary instruction produces a concrete result when a concrete operand completely determines the result, regardless of the other operand's value. These exceptions take precedence over the default rule.

Instruction	Condition
imul	either operand is a concrete 0
iand	either operand is a concrete 0
ior	either operand is a concrete value with all bits set

Note

This table is exhaustive. No other WebAssembly instruction has a concrete operand that completely determines the result. Shifts and rotates do not qualify because the shift amount is taken modulo the bit width. Division does not qualify because the result depends on whether the divisor is zero. The select instruction has its own rule (see Select).

Select

The select instruction is an exception to the default rule. If the condition is concrete, the result has the taint of the selected operand — the unselected operand's taint is ignored. If the condition is symbolic, the result is symbolic.

Constants

Constant instructions produce concrete values.

Memory

Each byte in the guest's linear memory is either concrete or symbolic.

Initialization

All bytes in linear memory are initially concrete, including bytes initialized by data segments.

Writes

When a value is stored to linear memory, the written bytes inherit the taint of the stored value.

Loads

When bytes are loaded from linear memory, the resulting value inherits the taint of the bytes read. If any byte in the range is symbolic, the result is symbolic.

Growth

When linear memory is grown via memory.grow, the newly allocated pages are concrete.

Copy

When bytes are copied via memory.copy, each destination byte inherits the taint of the corresponding source byte.

Fill

When bytes are written via memory.fill, each destination byte inherits the taint of the fill value.

Globals

Each global variable in the store has a taint (concrete or symbolic).

Initialization

All globals are initially concrete.

Sets

When a value is written to a mutable global via global.set, the global's taint is set to the taint of the written value.

Gets

When a value is read from a global via global.get, the resulting value inherits the taint of the global.

Locals

Each local variable in a function activation has a taint.

Initialization

Parameters receive their taint from the corresponding tagged argument at the invocation boundary: public arguments are concrete, private and blind arguments are symbolic. Locally declared variables are initialized to their default value and are concrete.

Sets

When a value is written to a local via local.set or local.tee, the local's taint is set to the taint of the written value.

Gets

When a value is read from a local via local.get, the resulting value inherits the taint of the local.

Tables

Table elements are references (funcref, externref). Table elements are not subject to taint tracking.

Invocation

Call Configuration

A call configuration is specified from the local party's perspective. It consists of:

1. The name of an exported function
2. A list of tagged arguments, one per parameter in the function's type signature

Each tagged argument is one of:

• Public — the value is known to both parties. The caller provides the value.
• Private — the value is known only to the local party. The caller provides the value.
• Blind — the value is provided by the remote party. The caller does not know it and supplies only the type.

A blind argument is the local party's declaration that a parameter slot is filled by the remote party. The same value is private from the remote party's perspective. Both parties MUST agree on which parameters are public and which are provided by each party; they differ only in which arguments they tag as private vs. blind.

The guest module does not observe the visibility of its inputs.

Note

For example, a call configuration for a two-party multiplication might look like:

// Illustrative, not normative.
enum Arg {
    Public(Value),
    Private(Value),
    Blind(ValType),
}

// Local party's call configuration
CallConfiguration {
    function: "multiply",
    args: [
        Arg::Private(Value::I32(7)),
        Arg::Blind(ValType::I32),
    ],
}

// Remote party's call configuration for the same invocation
CallConfiguration {
    function: "multiply",
    args: [
        Arg::Blind(ValType::I32),
        Arg::Private(Value::I32(5)),
    ],
}

The local party provides 7 as a private input and declares the second parameter as blind. The remote party provides 5 as a private input and declares the first parameter as blind. The guest function receives both as ordinary i32 parameters.

Return Values

The return values of a function are concrete. The embedder implicitly reveals any symbolic return values at the invocation boundary. Both parties observe the same return values, regardless of the taint those values had during execution.

Traps

A WebAssembly trap is a valid execution outcome. Both parties observe the same trap outcome. A trap is distinguishable from normal completion.

Sources of traps include those defined by WebAssembly:

• unreachable instruction
• Integer division by zero
• Out-of-bounds memory access
• Out-of-bounds table access
• Stack overflow

An abort is distinct from a trap and is implementation-defined (see Aborts).

Guest Module

A conforming guest module is a standard WebAssembly module. No special annotations or modifications are required.

Exports

The guest module exports standard WebAssembly functions. These functions are invoked as described in Invocation.

Supported parameter and return types:

• i32, i64 — Wasm core integer types
• f32, f64 — optional; see Floating-Point

Complex data structures MUST be passed via linear memory with appropriate serialization.

Imports

The guest module MAY import host functions. The set of host functions available to a module is implementation-defined.

Each host function MUST define how taint propagates through its parameters and return values. Embedders MAY provide host functions for accelerated operations (e.g., hash functions, signature verification).

Custom Sections

Implementations MAY interpret WebAssembly custom sections to guide optimization or transformation (e.g., range hints, loop bounds). Custom sections MUST NOT alter execution semantics — they are advisory only.

Determinism

Two conforming embedders MUST produce the same output — either the same return values, or a trap under the same condition — given:

1. The same guest module
2. The same call configuration
3. The same set of enabled WebAssembly features

This guarantee holds for all programs that stay within the resource limits of both embedders.

For cross-embedder compatibility, embedders MUST support the same set of WebAssembly features. The enabled feature set is part of the execution configuration — enabling or disabling a feature can change which modules are valid and how they execute.

Embedders that support WebAssembly proposals beyond the core specification MUST preserve determinism for all features they enable.

Floating-Point

Floating-point support is optional. Embedders that support floating-point MUST produce deterministic results by canonicalizing all NaN outputs to the canonical NaN defined by the WebAssembly specification. This eliminates the only source of nondeterminism in the WebAssembly core instruction set.

Resource Limits

Embedders MAY impose limits on resources such as stack depth and linear memory size. These limits are a source of cross-embedder divergence.

Embedders SHOULD declare their resource limits. For cross-embedder compatibility, embedders SHOULD use consistent resource limits.

Embedding

A verifiable compute embedder interacts with the WebAssembly semantics through the operations defined in this section. These operations replace their WebAssembly embedding counterparts where this specification defines different semantics. For all other operations — including module_decode, module_validate, module_instantiate, and module_exports — the corresponding WebAssembly embedding operations apply without modification.

Errors and Outcomes

Failure of an interface operation is indicated by one of:

• error — the operation failed (e.g., out-of-bounds access, invalid arguments).
• trap — the guest execution trapped.
• abort — the joint execution could not complete, for reasons outside the caller's control and outside the WebAssembly semantics (see Aborts).

Tagged Argument

A tagged argument pairs a visibility with either a value or a type:

• public(val) — a public value.
• private(val) — a private value provided by the local party.
• blind(valtype) — a value of the given type, provided by the remote party.

Invocation

invoke(store, funcaddr, tagged_arg*) : (store, val* | trap | abort | error)

1. Pre-condition: the function address funcaddr is valid in store.
2. Pre-condition: the number and types of tagged_arg* match the function's type signature.
3. Execute the function with the given tagged arguments. Each argument's visibility is consumed by the embedder. The guest receives the values as normal parameters.
4. If execution completes normally, let result be the return values. Return values are concrete.
5. If execution traps, let result be trap.
6. If the joint execution cannot complete, let result be abort.
7. Return the new store paired with result.

Memory

mem_write(store, memaddr, i: u32, byte, visibility) : (store | abort | error)

1. Pre-condition: the memory address memaddr is valid in store.
2. If i is out of bounds, return error.
3. Write byte at index i. Update the store: public maps to concrete, private and blind map to symbolic.
4. Return the updated store.

mem_read(store, memaddr, i: u32) : (byte | abort | error)

1. Pre-condition: the memory address memaddr is valid in store.
2. If i is out of bounds, return error.
3. If the byte at index i is symbolic, return error.
4. Return the byte at index i.

mem_reveal(store, memaddr, i: u32, n: u32) : (store | abort | error)

1. Pre-condition: the memory address memaddr is valid in store.
2. Pre-condition: both parties agree to reveal the specified region.
3. If i + n is out of bounds, return error.
4. Set the taint of bytes i through i + n − 1 to concrete.
5. Return the updated store.

Note

mem_reveal requires agreement from both parties. The mechanism for reaching this agreement is outside the scope of this specification. After a successful mem_reveal, the revealed bytes can be read via mem_read.

Implementation-Defined Behaviors

Implementation-defined behaviors MUST NOT alter WebAssembly execution semantics. When an embedder encounters an operation it does not support, it MUST NOT produce a WebAssembly trap. Instead, the embedder MUST report an abort, which is distinguishable from both normal completion and a trap (see Aborts).

Note

The following is a non-exhaustive list of areas where embedders commonly differ. It is advisory, not normative. Embedders SHOULD document their choices in these and any other areas where their behavior is implementation-defined.

Control Flow on Symbolic Values

Whether control flow can depend on symbolic inputs.

Note

;; May or may not be supported depending on the embedder
(if (local.get $private_condition)
  (then ...)
  (else ...))

Some embedders require all branch conditions to be concrete. Others support branching on symbolic values.

Symbolic Addressing

Whether memory addresses can depend on symbolic inputs.

Note

;; May or may not be supported
(i32.load (local.get $private_address))

Some embedders require concrete addresses. Others support address patterns that depend on symbolic values.

Input Allocation

The mechanism by which the embedder allocates space within the guest's linear memory for memory writes (see Embedding — Memory).

Aborts

How aborts are reported. An abort is distinct from both normal completion and a WebAssembly trap (see Traps). Sources include unsupported operations and failures in the cooperation between parties.

Host Functions

The set of host functions available to the guest module (see Imports).

Resource Limits

Limits on resources such as stack depth and linear memory size (see Resource Limits).

End of Specification