From 00dd745ef276c7d55ef4740942d3a6640d6b78a9 Mon Sep 17 00:00:00 2001
From: "Marcus (agent-cos)" <cos@marcus.local>
Date: Sat, 9 May 2026 22:03:06 -0700
Subject: [PATCH] =?UTF-8?q?refactor:=20remove=20WAT/WASM=20generator=20(su?=
 =?UTF-8?q?perseded=20by=20IR=E2=86=92Rust=E2=86=92WASM=20path)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Deleted compiler/src/generators/wasm.ts (472 lines)
- Deleted compiler/src/runtime/wasm-host.ts (165 lines)
- Deleted compiler/__tests__/e2e-wasm.test.ts (203 lines)
- Removed WASM import and generation call from compiler/src/index.ts
- Removed WASMGenerated from TS generator state enum literals
- Removed WASM codegen tests from parser.test.ts
- All 37 tests passing

The WASM generator was architecturally wrong: every Map/Set operation
crossed the WASM→JS boundary, creating 45-55% overhead for a module
that doesn't compute anything. WASM will be a byproduct of the Rust
backend via wasm-pack instead (M2.1).

Closes #19
---
 .gitignore                                    |   1 +
 compiler/__tests__/e2e-wasm.test.ts           | 203 --------
 compiler/__tests__/parser.test.ts             |  71 ---
 .../node_modules/.vite/vitest/results.json    |   2 +-
 .../generators/typescript-state-machine.ts    |   4 +-
 compiler/src/generators/wasm.ts               | 472 ------------------
 compiler/src/index.ts                         |   5 +-
 compiler/src/runtime/wasm-host.ts             | 165 ------
 compiler/test-output/RetryHandler.prov.jsonld |   2 +-
 .../test-output/RetryHandler.specbom.cdx.json |   6 +-
 .../RetryHandler.specbom.spdx.json            |   4 +-
 examples/Paxos.speck                          | 131 +++++
 examples/PreconditionTest.speck               |  22 +
 examples/Raft.speck                           | 272 ++++++++++
 reference-agent/src/types.ts                  |   2 +-
 15 files changed, 437 insertions(+), 925 deletions(-)
 create mode 100644 .gitignore
 delete mode 100644 compiler/__tests__/e2e-wasm.test.ts
 delete mode 100644 compiler/src/generators/wasm.ts
 delete mode 100644 compiler/src/runtime/wasm-host.ts
 create mode 100644 examples/Paxos.speck
 create mode 100644 examples/PreconditionTest.speck
 create mode 100644 examples/Raft.speck

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..89f9ac0
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+out/
diff --git a/compiler/__tests__/e2e-wasm.test.ts b/compiler/__tests__/e2e-wasm.test.ts
deleted file mode 100644
index aef5625..0000000
--- a/compiler/__tests__/e2e-wasm.test.ts
+++ /dev/null
@@ -1,203 +0,0 @@
-import { describe, it, expect } from 'vitest';
-import { parseSpeckContent } from '../src/parser.js';
-import { generateWASM } from '../src/generators/wasm.js';
-import { createHostImports, bindMemory, readScalarState } from '../src/runtime/wasm-host.js';
-import fs from 'fs';
-import path from 'path';
-import os from 'os';
-
-// Dynamic import wabt since it's a CommonJS module
-async function loadWabt() {
-  const wabt = await import('wabt');
-  return wabt.default();
-}
-
-describe('SpeckDL WASM E2E', () => {
-  it('should compile Counter speck to WAT, assemble to WASM, and run in Node.js', async () => {
-    // A minimal scalar-only speck that we can fully compile and run
-    // NOTE: Parser requires braces on the SAME line as block keywords
-    const speckSource = `speck Counter {
-  author: "Speckl Compiler v0.3"
-  source: document ref "WASM-E2E"
-  review: automated
-
-  state: {
-    count: Nat := 0
-    maxCount: Nat := 10
-  }
-
-  init: {
-    count := 0
-    maxCount := 10
-  }
-
-  action Increment() {
-    require count < maxCount
-    count := count + 1
-  }
-
-  action Decrement() {
-    require count > 0
-    count := count - 1
-  }
-
-  action Reset() {
-    count := 0
-  }
-
-  action GetCount() {
-    return count
-  }
-}`;
-
-    // 1. Parse
-    const ast = parseSpeckContent(speckSource);
-    expect(ast.specks).toHaveLength(1);
-    expect(ast.specks[0].name).toBe('Counter');
-
-    // 2. Generate WAT to temp dir
-    const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), 'speckl-wasm-e2e-'));
-    generateWASM(ast, tmpDir);
-
-    const watPath = path.join(tmpDir, 'Counter.wat');
-    expect(fs.existsSync(watPath)).toBe(true);
-
-    const watContent = fs.readFileSync(watPath, 'utf-8');
-    expect(watContent).toContain('(module');
-    expect(watContent).toContain('(export "init")');
-    expect(watContent).toContain('(export "Increment")');
-    expect(watContent).toContain('(export "Decrement")');
-    expect(watContent).toContain('(export "Reset")');
-    expect(watContent).toContain('(export "GetCount")');
-    expect(watContent).toContain('(export "getState")');
-    expect(watContent).toContain('(export "memory")');
-
-    // 3. Assemble WAT → WASM using wabt
-    const wabtModule = await loadWabt();
-    const wasmModule = wabtModule.parseWat('Counter.wat', watContent);
-    wasmModule.resolveNames();
-    wasmModule.validate({ features: {} });
-    const binaryOutput = wasmModule.toBinary({ log: false, write_debug_names: false });
-    const wasmBytes = binaryOutput.buffer;
-
-    expect(wasmBytes.length).toBeGreaterThan(0);
-    expect(wasmBytes.length).toBeGreaterThan(50); // Not just empty header
-
-    // 4. Instantiate with host runtime
-    const hostState = {
-      maps: new Map(),
-      sets: new Map(),
-      nextHandle: 1,
-      memory: null as WebAssembly.Memory | null,
-    };
-    const imports = { speckl: createHostImports(hostState) };
-
-    const wasm = await WebAssembly.instantiate(wasmBytes, imports);
-    const memory = wasm.instance.exports.memory as WebAssembly.Memory;
-    bindMemory(hostState, memory);
-
-    // 5. Verify exports
-    expect(typeof wasm.instance.exports.init).toBe('function');
-    expect(typeof wasm.instance.exports.Increment).toBe('function');
-    expect(typeof wasm.instance.exports.Decrement).toBe('function');
-    expect(typeof wasm.instance.exports.Reset).toBe('function');
-    expect(typeof wasm.instance.exports.GetCount).toBe('function');
-    expect(typeof wasm.instance.exports.getState).toBe('function');
-    expect(memory).toBeInstanceOf(WebAssembly.Memory);
-
-    // 6. Run init
-    (wasm.instance.exports.init as Function)();
-
-    // 7. Verify initial state via getState
-    const stateResult = (wasm.instance.exports.getState as Function)();
-    // getState returns i32 i32 (ptr, len)
-    expect(stateResult).toBeDefined();
-
-    // Read memory directly to verify state
-    const scalarState = readScalarState(memory, ['count', 'maxCount']);
-    expect(scalarState.count).toBe(0);
-    expect(scalarState.maxCount).toBe(10);
-
-    // 8. Run Increment 3 times, calling getState after each to sync memory
-    for (let i = 0; i < 3; i++) {
-      const ret = (wasm.instance.exports.Increment as Function)();
-      expect(ret).toBe(1); // Success
-      (wasm.instance.exports.getState as Function)(); // Sync globals to memory
-    }
-
-    const afterIncrement = readScalarState(memory, ['count', 'maxCount']);
-    expect(afterIncrement.count).toBe(3);
-    expect(afterIncrement.maxCount).toBe(10);
-
-    // 9. Run Decrement once
-    const decRet = (wasm.instance.exports.Decrement as Function)();
-    expect(decRet).toBe(1); // Success
-    (wasm.instance.exports.getState as Function)();
-
-    const afterDecrement = readScalarState(memory, ['count', 'maxCount']);
-    expect(afterDecrement.count).toBe(2);
-
-    // 10. Run GetCount — should return current count (global, not memory)
-    const getRet = (wasm.instance.exports.GetCount as Function)();
-    expect(getRet).toBe(2);
-
-    // 11. Run Reset
-    const resetRet = (wasm.instance.exports.Reset as Function)();
-    expect(resetRet).toBe(1); // Success
-    (wasm.instance.exports.getState as Function)();
-
-    const afterReset = readScalarState(memory, ['count', 'maxCount']);
-    expect(afterReset.count).toBe(0);
-
-    // 12. Guard test: Decrement at 0 should fail
-    const guardFail = (wasm.instance.exports.Decrement as Function)();
-    expect(guardFail).toBe(0); // Guard failed → return 0
-
-    // 13. Guard test: Increment at maxCount should fail
-    // First increment to max
-    for (let i = 0; i < 10; i++) {
-      (wasm.instance.exports.Increment as Function)();
-    }
-    (wasm.instance.exports.getState as Function)();
-    const atMax = readScalarState(memory, ['count', 'maxCount']);
-    expect(atMax.count).toBe(10);
-
-    const maxGuardFail = (wasm.instance.exports.Increment as Function)();
-    expect(maxGuardFail).toBe(0); // Guard failed → return 0
-
-    // Cleanup
-    fs.rmSync(tmpDir, { recursive: true, force: true });
-  }, 30000); // 30s timeout for wabt compilation
-
-  it('should compile TigerBeetle speck to valid WAT that wabt accepts', async () => {
-    // Load the full TigerBeetle speck from file
-    const speckPath = path.join(__dirname, 'tigerbeetle.speck');
-    const speckSource = fs.readFileSync(speckPath, 'utf-8');
-
-    const ast = parseSpeckContent(speckSource);
-    expect(ast.specks).toHaveLength(1);
-    expect(ast.specks[0].name).toBe('TigerBeetle');
-
-    const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), 'speckl-wasm-e2e-tb-'));
-    generateWASM(ast, tmpDir);
-
-    const watPath = path.join(tmpDir, 'TigerBeetle.wat');
-    expect(fs.existsSync(watPath)).toBe(true);
-
-    const watContent = fs.readFileSync(watPath, 'utf-8');
-
-    // Validate with wabt
-    const wabtModule = await loadWabt();
-    const wasmModule = wabtModule.parseWat('TigerBeetle.wat', watContent);
-
-    // These should not throw
-    wasmModule.resolveNames();
-    wasmModule.validate({ features: {} });
-    const binaryOutput = wasmModule.toBinary({ log: false, write_debug_names: false });
-
-    expect(binaryOutput.buffer.length).toBeGreaterThan(100);
-
-    // Cleanup
-    fs.rmSync(tmpDir, { recursive: true, force: true });
-  }, 30000);
-});
diff --git a/compiler/__tests__/parser.test.ts b/compiler/__tests__/parser.test.ts
index 58af7b0..1673982 100644
--- a/compiler/__tests__/parser.test.ts
+++ b/compiler/__tests__/parser.test.ts
@@ -1,6 +1,5 @@
 import { describe, it, expect } from 'vitest';
 import { parseSpeckContent, parseSpeckFile } from '../src/parser.js';
-import { generateWASM } from '../src/generators/wasm.js';
 
 describe('SpeckDL Parser', () => {
   describe('parseSpeckContent', () => {
@@ -526,75 +525,5 @@ speck Second {
     });
   });
 
-  describe('WASM Codegen', () => {
-    it('should generate WAT for TigerBeetle with all exports', () => {
-      const ast = parseSpeckFile('./__tests__/tigerbeetle.speck');
-      const fs = require('fs');
-      const os = require('os');
-      const path = require('path');
-      const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), 'speckl-wasm-test-'));
 
-      generateWASM(ast, tmpDir);
-
-      const watPath = path.join(tmpDir, 'TigerBeetle.wat');
-      expect(fs.existsSync(watPath)).toBe(true);
-
-      const wat = fs.readFileSync(watPath, 'utf-8');
-
-      // Module structure
-      expect(wat).toContain('(module');
-      expect(wat).toContain('(memory (export "memory")');
-
-      // Host imports
-      expect(wat).toContain('(import "speckl" "map_create"');
-      expect(wat).toContain('(import "speckl" "set_create"');
-
-      // State globals
-      expect(wat).toContain('(global $nextId');
-      expect(wat).toContain('(global $accounts');
-      expect(wat).toContain('(global $transfers');
-      expect(wat).toContain('(global $ledgerOpen');
-
-      // init export
-      expect(wat).toContain('(func $init (export "init")');
-
-      // Action exports
-      expect(wat).toContain('(func $CreateAccount (export "CreateAccount")');
-      expect(wat).toContain('(func $Transfer (export "Transfer")');
-      expect(wat).toContain('(func $CloseAccount (export "CloseAccount")');
-      expect(wat).toContain('(func $CloseLedger (export "CloseLedger")');
-
-      // getState export
-      expect(wat).toContain('(func $getState (export "getState")');
-
-      // Constraint stub
-      expect(wat).toContain('(func $checkConstraints (export "checkConstraints")');
-
-      // Scalar init values
-      expect(wat).toContain('(i32.const 1)'); // nextId default
-      expect(wat).toContain('(call $map_create)');
-      expect(wat).toContain('(call $set_create)');
-
-      fs.rmSync(tmpDir, { recursive: true });
-    });
-
-    it('should emit scalar guard expressions as WASM comparison', () => {
-      const ast = parseSpeckFile('./__tests__/tigerbeetle.speck');
-      const fs = require('fs');
-      const os = require('os');
-      const path = require('path');
-      const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), 'speckl-wasm-test-'));
-
-      generateWASM(ast, tmpDir);
-      const wat = fs.readFileSync(path.join(tmpDir, 'TigerBeetle.wat'), 'utf-8');
-
-      // ledgerOpen == true should compile to i32.eq
-      expect(wat).toContain('(i32.eq (global.get $ledgerOpen) (i32.const 1))');
-
-      // nextId + 1 should compile to i32.add
-      expect(wat).toContain('(i32.add (global.get $nextId) (i32.const 1))');
-
-      fs.rmSync(tmpDir, { recursive: true });
-    });
-  });
 });
diff --git a/compiler/node_modules/.vite/vitest/results.json b/compiler/node_modules/.vite/vitest/results.json
index a6ca69e..9cc7a70 100644
--- a/compiler/node_modules/.vite/vitest/results.json
+++ b/compiler/node_modules/.vite/vitest/results.json
@@ -1 +1 @@
-{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":40.638667,"failed":false}],[":__tests__/e2e-wasm.test.ts",{"duration":25.08648199999999,"failed":true}],[":src/__tests__/compiler.test.ts",{"duration":13.108581000000015,"failed":false}]]}
\ No newline at end of file
+{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":37.17850800000002,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":10.335649000000046,"failed":false}]]}
\ No newline at end of file
diff --git a/compiler/src/generators/typescript-state-machine.ts b/compiler/src/generators/typescript-state-machine.ts
index 85f9912..63739fe 100644
--- a/compiler/src/generators/typescript-state-machine.ts
+++ b/compiler/src/generators/typescript-state-machine.ts
@@ -305,7 +305,7 @@ function rewriteExpr(expr: string, stateVarNames: Set<string>, localNames: Set<s
   // Step 2: Replace state enum literals with enum refs BEFORE identifier replacement
   const allStateValues = new Set<string>(knownStateValues);
   // Add common fallback states
-  ['Open','Grooming','Groomed','Assigned','InProgress','InReview','Merged','Blocked','Closed','Idle','Parsing','Parsed','ProvenanceGenerated','BOMsGenerated','TypeScriptGenerated','WASMGenerated','Done'].forEach(s => allStateValues.add(s));
+  ['Open','Grooming','Groomed','Assigned','InProgress','InReview','Merged','Blocked','Closed','Idle','Parsing','Parsed','ProvenanceGenerated','BOMsGenerated','TypeScriptGenerated','Done'].forEach(s => allStateValues.add(s));
   if (allStateValues.size > 0) {
     const stateValueRegex = new RegExp('\\b(' + Array.from(allStateValues).join('|') + ')\\b', 'g');
     ts = ts.replace(stateValueRegex, `${stateEnumName}.$1`);
@@ -361,7 +361,7 @@ function cleanName(s: string): string {
 
 function replaceStateWithEnum(expr: string, enumName: string, knownStateValues: string[]): string {
   const allStateValues = new Set<string>(knownStateValues);
-  ['Open','Grooming','Groomed','Assigned','InProgress','InReview','Merged','Blocked','Closed','Idle','Parsing','Parsed','ProvenanceGenerated','BOMsGenerated','TypeScriptGenerated','WASMGenerated','Done'].forEach(s => allStateValues.add(s));
+  ['Open','Grooming','Groomed','Assigned','InProgress','InReview','Merged','Blocked','Closed','Idle','Parsing','Parsed','ProvenanceGenerated','BOMsGenerated','TypeScriptGenerated','Done'].forEach(s => allStateValues.add(s));
   if (allStateValues.size === 0) return expr;
   const stateValueRegex = new RegExp('\\b(' + Array.from(allStateValues).join('|') + ')\\b', 'g');
   return expr.replace(stateValueRegex, `${enumName}.$1`);
diff --git a/compiler/src/generators/wasm.ts b/compiler/src/generators/wasm.ts
deleted file mode 100644
index 700ddc1..0000000
--- a/compiler/src/generators/wasm.ts
+++ /dev/null
@@ -1,472 +0,0 @@
-import { AST, SpeckNode, StateNode, InitNode, ActionNode, EventNode } from '../parser.js';
-import fs from 'fs';
-import path from 'path';
-
-/**
- * Generate WebAssembly Text (WAT) from a SpeckDL state machine spec.
- *
- * Emits a .wat file per speck with:
- *   - Linear memory for scalar state (Nat/Int/Real/Bool)
- *   - Imported host functions for Map<K,V> and Set<T>
- *   - Exported `init()` — calls host to init Maps/Sets + sets scalars
- *   - Exported action functions (one per action)
- *   - Exported `getState()` — serializes scalars into memory
- *   - Exported `checkConstraints()` — runtime guard stubs
- *
- * Compile to .wasm with: wat2wasm <file>.wat -o <file>.wasm
- *
- * Host runtime (JS): see `speckl/runtime/wasm-host.js`
- */
-
-// ---------------------------------------------------------------------------
-// Host imports required by generated modules
-// ---------------------------------------------------------------------------
-const HOST_IMPORTS = [
-  '(import "speckl" "map_create" (func $map_create (result i32)))',
-  '(import "speckl" "map_set" (func $map_set (param i32 i32 i32)))',
-  '(import "speckl" "map_get" (func $map_get (param i32 i32) (result i32)))',
-  '(import "speckl" "map_has" (func $map_has (param i32 i32) (result i32)))',
-  '(import "speckl" "map_remove" (func $map_remove (param i32 i32)))',
-  '(import "speckl" "set_create" (func $set_create (result i32)))',
-  '(import "speckl" "set_add" (func $set_add (param i32 i32)))',
-  '(import "speckl" "set_has" (func $set_has (param i32 i32) (result i32)))',
-  '(import "speckl" "set_size" (func $set_size (param i32) (result i32)))',
-  '(import "speckl" "alloc" (func $alloc (param i32) (result i32)))',
-  '(import "speckl" "write_i32" (func $write_i32 (param i32 i32)))',
-  '(import "speckl" "write_f64" (func $write_f64 (param i32 f64)))',
-];
-
-export function generateWASM(ast: AST, outputDir: string): void {
-  for (const speck of ast.specks) {
-    const hasStateMachine = speck.members.some(m =>
-      m.type === 'state' || m.type === 'init' || m.type === 'action'
-    );
-    if (!hasStateMachine) continue;
-
-    const wat = emitSpeckWAT(speck);
-    const filename = `${speck.name}.wat`;
-    const filepath = path.join(outputDir, filename);
-    fs.writeFileSync(filepath, wat);
-    console.log(`Generated WAT: ${filepath}`);
-  }
-}
-
-function emitSpeckWAT(speck: SpeckNode): string {
-  const stateNode = speck.members.find(m => m.type === 'state') as StateNode | undefined;
-  const initNode  = speck.members.find(m => m.type === 'init') as InitNode | undefined;
-  const actions   = speck.members.filter(m => m.type === 'action') as ActionNode[];
-  const events    = speck.members.filter(m => m.type === 'event') as EventNode[];
-
-  const stateVars = stateNode?.variables ?? [];
-
-  // -------------------------------------------------------------------------
-  // 1. Memory layout for scalar state variables
-  // -------------------------------------------------------------------------
-  // Each scalar gets 8 bytes (i64/f64 slot). Map/Set handles are i32 refs
-  // stored in globals.
-  //
-  // Layout: [0..8) var0, [8..16) var1, ... then string pool for getState()
-  //
-  const scalarVars = stateVars.filter(v => isScalarType(v.typeExpr));
-  const refVars    = stateVars.filter(v => !isScalarType(v.typeExpr));
-
-  const memSize = Math.max(1, Math.ceil((scalarVars.length * 8 + 1024) / 65536));
-
-  // -------------------------------------------------------------------------
-  // 2. Globals: one per state variable
-  // -------------------------------------------------------------------------
-  const globals = stateVars.map((v, i) => {
-    if (isScalarType(v.typeExpr)) {
-      const wasmType = wasmTypeOf(v.typeExpr);
-      const initVal = initValueFor(v.name, v.typeExpr, v.defaultInit, initNode);
-      return `(global $${v.name} (mut ${wasmType}) (${wasmType}.const ${initVal}))`;
-    } else {
-      // Map or Set — store as i32 handle (0 = uninitialized)
-      return `(global $${v.name} (mut i32) (i32.const 0))`;
-    }
-  }).join('\n');
-
-  // -------------------------------------------------------------------------
-  // 3. init() export
-  // -------------------------------------------------------------------------
-  const initBody = emitInitBody(stateVars, initNode);
-
-  // -------------------------------------------------------------------------
-  // 4. Action exports
-  // -------------------------------------------------------------------------
-  const actionFuncs = actions.map(a => emitActionWAT(a, stateVars)).join('\n\n');
-
-  // -------------------------------------------------------------------------
-  // 5. getState() export — write scalars to memory, return ptr+len
-  // -------------------------------------------------------------------------
-  const getStateBody = emitGetState(scalarVars);
-
-  // -------------------------------------------------------------------------
-  // 6. checkConstraints() stub
-  // -------------------------------------------------------------------------
-  const checkConstraints = `
-  ;; checkConstraints — runtime constraint evaluation stub
-  (func $checkConstraints (export "checkConstraints") (result i32)
-    ;; TODO: evaluate constraint expressions at runtime
-    (i32.const 1)
-  )`;
-
-  // -------------------------------------------------------------------------
-  // 7. Assemble module
-  // -------------------------------------------------------------------------
-  const module =
-    `;; Auto-generated by speckl-compile from ${speck.name}\n` +
-    `;; Compile: wat2wasm ${speck.name}.wat -o ${speck.name}.wasm\n\n` +
-    `(module\n` +
-    `  ;; Host imports for Map/Set/alloc\n` +
-    `  ${HOST_IMPORTS.join('\n  ')}\n\n` +
-    `  ;; Linear memory (exported so host can read state)\n` +
-    `  (memory (export "memory") ${memSize})\n\n` +
-    `  ;; State globals\n` +
-    `  ${globals}\n\n` +
-    `  ;; ---- init ----\n` +
-    `  (func $init (export "init")\n` +
-    `    ${initBody}\n` +
-    `  )\n\n` +
-    `  ;; ---- Actions ----\n` +
-    `  ${actionFuncs}\n\n` +
-    `  ;; ---- getState ----\n` +
-    `  (func $getState (export "getState") (result i32 i32)\n` +
-    `    ${getStateBody}\n` +
-    `  )\n\n` +
-    `  ${checkConstraints}\n` +
-    `)`;
-
-  return module;
-}
-
-// =============================================================================
-// init() body generation
-// =============================================================================
-function emitInitBody(
-  stateVars: StateNode['variables'],
-  initNode: InitNode | undefined
-): string {
-  const lines: string[] = [];
-
-  for (const v of stateVars) {
-    if (isScalarType(v.typeExpr)) {
-      const val = initValueFor(v.name, v.typeExpr, v.defaultInit, initNode);
-      const wasmType = wasmTypeOf(v.typeExpr);
-      lines.push(`(${wasmType}.const ${val})`);
-      lines.push(`(global.set $${v.name})`);
-    } else if (isMapType(v.typeExpr)) {
-      lines.push(`(call $map_create)`);
-      lines.push(`(global.set $${v.name})`);
-    } else if (isSetType(v.typeExpr)) {
-      lines.push(`(call $set_create)`);
-      lines.push(`(global.set $${v.name})`);
-    }
-  }
-
-  return lines.join('\n    ');
-}
-
-// =============================================================================
-// Action function generation
-// =============================================================================
-function emitActionWAT(action: ActionNode, stateVars: StateNode['variables']): string {
-  const scalarStateNames = new Set(
-    stateVars.filter(v => isScalarType(v.typeExpr)).map(v => v.name)
-  );
-  const mapStateNames = new Set(
-    stateVars.filter(v => isMapType(v.typeExpr)).map(v => v.name)
-  );
-  const setStateNames = new Set(
-    stateVars.filter(v => isSetType(v.typeExpr)).map(v => v.name)
-  );
-
-  // Params: SpeckDL Nat/Int → i32, Real → f64, Bool → i32
-  const params = action.params.map(p => {
-    const t = wasmTypeOf(p.type);
-    return `(param $${p.name} ${t})`;
-  }).join(' ');
-
-  const localLines: string[] = [];
-  const bodyLines: string[] = [];
-
-  for (const stmt of action.statements) {
-    switch (stmt.type) {
-      case 'require': {
-        // Emit guard: if !condition → return 0 (failure indicator)
-        // For now, require guards that reference only scalar state variables
-        // and simple comparisons are emitted. Complex ones trap/return 0.
-        const guard = emitGuardExpr(stmt.expr, scalarStateNames, mapStateNames, setStateNames);
-        bodyLines.push(`;; require: ${stmt.expr}`);
-        bodyLines.push(guard);
-        break;
-      }
-      case 'assign': {
-        bodyLines.push(`;; ${stmt.target} := ${stmt.expr}`);
-        bodyLines.push(emitAssignment(stmt.target, stmt.expr, scalarStateNames, mapStateNames));
-        break;
-      }
-      case 'let': {
-        // let name := expr — allocate local, compute expr, store
-        const wasmT = inferExprType(stmt.expr, scalarStateNames);
-        localLines.push(`(local $${stmt.name} ${wasmT})`);
-        bodyLines.push(emitExpr(stmt.expr, scalarStateNames));
-        bodyLines.push(`(local.set $${stmt.name})`);
-        break;
-      }
-      case 'emit': {
-        // emit → decision log push (host call stub for now)
-        bodyLines.push(`;; emit ${stmt.event} { ... }`);
-        // TODO: structured emit via host
-        break;
-      }
-      case 'return': {
-        bodyLines.push(emitExpr(stmt.expr, scalarStateNames));
-        bodyLines.push(`(return)`);
-        break;
-      }
-    }
-  }
-
-  // Default return: i32.const 1 for success if action returns void
-  const hasReturn = action.statements.some(s => s.type === 'return');
-  if (!hasReturn) {
-    bodyLines.push(`(i32.const 1)`);
-  }
-
-  const locals = localLines.length ? `\n    ${localLines.join('\n    ')}` : '';
-
-  return `  ;; action: ${action.name}\n` +
-    `  (func $${action.name} (export "${action.name}") ${params} (result i32)\n` +
-    `    ${locals}\n` +
-    `    ${bodyLines.join('\n    ')}\n` +
-    `  )`;
-}
-
-// =============================================================================
-// Expression / guard emission (simplified — covers common scalar patterns)
-// =============================================================================
-function emitGuardExpr(
-  expr: string,
-  scalars: Set<string>,
-  maps: Set<string>,
-  sets: Set<string>
-): string {
-  // Very simple pattern: "x >= 0", "x == true", "x != y", etc.
-  const m = expr.match(/^\s*(\w+)\s*(>=|<=|>|<|==|!=)\s*(.+?)\s*$/);
-  if (!m) {
-    // Can't compile guard — just comment, no stack effect
-    return `;; Complex guard not compiled: ${expr}`;
-  }
-
-  const [, left, op, rightRaw] = m;
-  const right = rightRaw.trim();
-
-  if (!scalars.has(left)) {
-    return `;; Guard on non-scalar not compiled: ${expr}`;
-  }
-
-  const lhs = `(global.get $${left})`;
-
-  // Parse right side
-  let rhs: string;
-  const rightNum = parseFloat(right);
-  if (!isNaN(rightNum)) {
-    rhs = `(i32.const ${rightNum})`;
-  } else if (right === 'true') {
-    rhs = `(i32.const 1)`;
-  } else if (right === 'false') {
-    rhs = `(i32.const 0)`;
-  } else if (scalars.has(right)) {
-    rhs = `(global.get $${right})`;
-  } else {
-    return `;; Complex right-hand side not compiled: ${expr}`;
-  }
-
-  const comparison = (() => {
-    switch (op) {
-      case '>=': return `(i32.ge_s ${lhs} ${rhs})`;
-      case '<=': return `(i32.le_s ${lhs} ${rhs})`;
-      case '>':  return `(i32.gt_s ${lhs} ${rhs})`;
-      case '<':  return `(i32.lt_s ${lhs} ${rhs})`;
-      case '==': return `(i32.eq ${lhs} ${rhs})`;
-      case '!=': return `(i32.ne ${lhs} ${rhs})`;
-      default:   return `(i32.const 1)`;
-    }
-  })();
-
-  // If guard fails (comparison is FALSE), return 0
-  return `${comparison}\n    (i32.eqz)\n    (if (then (return (i32.const 0))))`;
-}
-
-function emitExpr(expr: string, scalars: Set<string>): string {
-  // Handle: nextId + 1, nextId, numeric literals, etc.
-  expr = expr.trim();
-
-  // Simple numeric literal
-  const num = parseFloat(expr);
-  if (!isNaN(num) && !expr.match(/\w/)) {
-    return `(i32.const ${num})`;
-  }
-
-  // Simple variable reference
-  if (/^\w+$/.test(expr) && scalars.has(expr)) {
-    return `(global.get $${expr})`;
-  }
-
-  // Binary op: left + right, left - right, left * right
-  const binOp = expr.match(/^(\w+)\s*([+\-*/])\s*(.+)$/);
-  if (binOp) {
-    const [, left, op, right] = binOp;
-    const lhs = scalars.has(left) ? `(global.get $${left})` : `(i32.const ${parseFloat(left)})`;
-    const rhsNum = parseFloat(right.trim());
-    const rhs = isNaN(rhsNum)
-      ? (scalars.has(right.trim()) ? `(global.get $${right.trim()})` : `(i32.const 0) ;; uncompiled`)
-      : `(i32.const ${rhsNum})`;
-    switch (op) {
-      case '+': return `(i32.add ${lhs} ${rhs})`;
-      case '-': return `(i32.sub ${lhs} ${rhs})`;
-      case '*': return `(i32.mul ${lhs} ${rhs})`;
-      default:  return `(i32.const 0) ;; uncompiled op ${op}`;
-    }
-  }
-
-  return `(i32.const 0) ;; uncompiled expr: ${expr}`;
-}
-
-function inferExprType(expr: string, scalars: Set<string>): string {
-  // Default to i32; we could infer from variable types but that's future work
-  return 'i32';
-}
-
-function emitAssignment(
-  target: string,
-  expr: string,
-  scalars: Set<string>,
-  maps: Set<string>
-): string {
-  // Scalar assignment: this.x = expr
-  if (scalars.has(target)) {
-    return `${emitExpr(expr, scalars)}\n    (global.set $${target})`;
-  }
-
-  // Map assignment: accounts[id] := expr — host call
-  const mapAssign = target.match(/^(\w+)\[(.+)\]$/);
-  if (mapAssign && maps.has(mapAssign[1])) {
-    const mapName = mapAssign[1];
-    const keyExpr = mapAssign[2];
-    // For now: map_set(map_handle, key_handle, value_handle)
-    // This needs boxing; simplified version just marks as stub
-    return `;; Map assignment not yet compiled: ${target} := ${expr}`;
-  }
-
-  // Record field assignment: accounts[id].field := expr
-  const recordAssign = target.match(/^(\w+)\[(.+)\]\.(\w+)$/);
-  if (recordAssign && maps.has(recordAssign[1])) {
-    return `;; Record field assignment not yet compiled: ${target} := ${expr}`;
-  }
-
-  return `;; Unrecognized assignment target: ${target}`;
-}
-
-// =============================================================================
-// getState() — serialize scalar state to memory
-// =============================================================================
-function emitGetState(scalarVars: StateNode['variables']): string {
-  const lines: string[] = [];
-  let offset = 0;
-
-  for (const v of scalarVars) {
-    const t = wasmTypeOf(v.typeExpr);
-    if (t === 'i32') {
-      lines.push(`(i32.const ${offset})`);
-      lines.push(`(global.get $${v.name})`);
-      lines.push(`(i32.store)`);
-      offset += 4;
-    } else if (t === 'f64') {
-      lines.push(`(i32.const ${offset})`);
-      lines.push(`(global.get $${v.name})`);
-      lines.push(`(f64.store)`);
-      offset += 8;
-    } else {
-      // i64
-      lines.push(`(i32.const ${offset})`);
-      lines.push(`(global.get $${v.name})`);
-      lines.push(`(i64.store)`);
-      offset += 8;
-    }
-  }
-
-  // Return (ptr, len)
-  lines.push(`(i32.const 0)`);     // ptr = 0
-  lines.push(`(i32.const ${offset})`); // len = total bytes written
-
-  return lines.join('\n    ');
-}
-
-// =============================================================================
-// Type helpers
-// =============================================================================
-function isScalarType(t: any): boolean {
-  if (t.type === 'primitive') {
-    return ['Nat', 'Int', 'Real', 'Bool'].includes(t.name);
-  }
-  if (t.type === 'ident') return true; // opaque ident → i32 handle
-  return false;
-}
-
-function isMapType(t: any): boolean {
-  return t.type === 'map';
-}
-
-function isSetType(t: any): boolean {
-  return t.type === 'set';
-}
-
-function wasmTypeOf(t: any): string {
-  if (t.type === 'primitive') {
-    if (t.name === 'Nat') return 'i32';
-    if (t.name === 'Int') return 'i32';
-    if (t.name === 'Real') return 'f64';
-    if (t.name === 'Bool') return 'i32';
-    if (t.name === 'String') return 'i32'; // ptr
-    if (t.name === 'Bytes') return 'i32';  // ptr
-    return 'i32';
-  }
-  if (t.type === 'ident') return 'i32';
-  if (t.type === 'map') return 'i32';   // handle
-  if (t.type === 'set') return 'i32';  // handle
-  return 'i32';
-}
-
-function initValueFor(
-  varName: string,
-  typeExpr: any,
-  defaultInit: string | undefined,
-  initNode: InitNode | undefined
-): string {
-  // Use initNode assignment if present
-  const initAssign = initNode?.assignments.find(a => a.name === varName);
-  if (initAssign) {
-    const expr = initAssign.expr.trim();
-    if (expr === 'true') return '1';
-    if (expr === 'false') return '0';
-    if (expr === 'Map.empty()') return '0'; // will be replaced by host call
-    if (expr === 'Set.empty()') return '0';
-    const num = parseFloat(expr);
-    if (!isNaN(num)) return String(num);
-    return '0';
-  }
-
-  // Fallback to defaultInit
-  if (defaultInit) {
-    if (defaultInit === 'true') return '1';
-    if (defaultInit === 'false') return '0';
-    const num = parseFloat(defaultInit);
-    if (!isNaN(num)) return String(num);
-  }
-
-  // Default zero
-  if (typeExpr.type === 'primitive' && typeExpr.name === 'Real') return '0.0';
-  return '0';
-}
diff --git a/compiler/src/index.ts b/compiler/src/index.ts
index 87244a8..e71a6ea 100644
--- a/compiler/src/index.ts
+++ b/compiler/src/index.ts
@@ -7,7 +7,7 @@ import { generateProvenanceGraph } from './generators/provenance.js';
 import { generateCycloneDX } from './generators/cyclonedx.js';
 import { generateSPDX } from './generators/spdx.js';
 import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js';
-import { generateWASM } from './generators/wasm.js';
+
 import fs from 'fs';
 import path from 'path';
 
@@ -82,9 +82,6 @@ async function main() {
   console.log('\nGenerating TypeScript state machine...');
   generateTypeScriptStateMachine(ast, options.outputDir);
 
-  // Generate WASM state machine
-  console.log('\nGenerating WebAssembly (WAT)...');
-  generateWASM(ast, options.outputDir);
 
   // Generate BOM based on format selection
   if (options.bomFormat === 'cdx' || options.bomFormat === 'both') {
diff --git a/compiler/src/runtime/wasm-host.ts b/compiler/src/runtime/wasm-host.ts
deleted file mode 100644
index 513892b..0000000
--- a/compiler/src/runtime/wasm-host.ts
+++ /dev/null
@@ -1,165 +0,0 @@
-/**
- * Speckl WASM Host Runtime
- *
- * Provides JS-side implementations for imported host functions used by
- * Speckl-generated WASM modules:
- *   - map_create, map_set, map_get, map_has, map_remove
- *   - set_create, set_add, set_has, set_size
- *   - alloc, write_i32, write_f64
- *
- * Usage:
- *   const wasmModule = await WebAssembly.instantiate(bytes, {
- *     speckl: createHostImports()
- *   });
- *   wasmModule.exports.init();
- *   wasmModule.exports.CreateAccount(100.0);
- *   const state = getStateFromMemory(wasmModule);
- */
-
-interface HostState {
-  maps: Map<number, Map<number, any>>;
-  sets: Map<number, Set<any>>;
-  nextHandle: number;
-  memory: WebAssembly.Memory | null;
-}
-
-function createHostState(): HostState {
-  return {
-    maps: new Map(),
-    sets: new Map(),
-    nextHandle: 1,
-    memory: null,
-  };
-}
-
-export function createHostImports(state: HostState = createHostState()) {
-  return {
-    // ---- Map operations ----
-    map_create: (): number => {
-      const handle = state.nextHandle++;
-      state.maps.set(handle, new Map());
-      return handle;
-    },
-
-    map_set: (mapHandle: number, keyHandle: number, valueHandle: number): void => {
-      const map = state.maps.get(mapHandle);
-      if (!map) throw new Error(`Map handle ${mapHandle} not found`);
-      // For now, keys and values are simple i32 handles; boxing layer comes later
-      map.set(keyHandle, valueHandle);
-    },
-
-    map_get: (mapHandle: number, keyHandle: number): number => {
-      const map = state.maps.get(mapHandle);
-      if (!map) return 0;
-      return map.has(keyHandle) ? (map.get(keyHandle) ?? 0) : 0;
-    },
-
-    map_has: (mapHandle: number, keyHandle: number): number => {
-      const map = state.maps.get(mapHandle);
-      if (!map) return 0;
-      return map.has(keyHandle) ? 1 : 0;
-    },
-
-    map_remove: (mapHandle: number, keyHandle: number): void => {
-      const map = state.maps.get(mapHandle);
-      if (map) map.delete(keyHandle);
-    },
-
-    // ---- Set operations ----
-    set_create: (): number => {
-      const handle = state.nextHandle++;
-      state.sets.set(handle, new Set());
-      return handle;
-    },
-
-    set_add: (setHandle: number, valueHandle: number): void => {
-      const set = state.sets.get(setHandle);
-      if (!set) throw new Error(`Set handle ${setHandle} not found`);
-      set.add(valueHandle);
-    },
-
-    set_has: (setHandle: number, valueHandle: number): number => {
-      const set = state.sets.get(setHandle);
-      if (!set) return 0;
-      return set.has(valueHandle) ? 1 : 0;
-    },
-
-    set_size: (setHandle: number): number => {
-      const set = state.sets.get(setHandle);
-      if (!set) return 0;
-      return set.size;
-    },
-
-    // ---- Memory helpers ----
-    alloc: (size: number): number => {
-      // Simple bump allocator: for now, just return 0 (stack allocation handled by compiler)
-      // Future: maintain bump pointer in memory
-      return 0;
-    },
-
-    write_i32: (ptr: number, value: number): void => {
-      if (!state.memory) throw new Error('Memory not bound');
-      const view = new DataView(state.memory.buffer);
-      view.setInt32(ptr, value, true); // little-endian
-    },
-
-    write_f64: (ptr: number, value: number): void => {
-      if (!state.memory) throw new Error('Memory not bound');
-      const view = new DataView(state.memory.buffer);
-      view.setFloat64(ptr, value, true);
-    },
-  };
-}
-
-/**
- * Bind a WASM memory export to the host state so write_i32/write_f64 work.
- */
-export function bindMemory(state: HostState, memory: WebAssembly.Memory): void {
-  state.memory = memory;
-}
-
-/**
- * Read scalar state from WASM memory after getState() has been called.
- * Layout matches emitGetState(): [nextId: i32][ledgerOpen: i32]...
- */
-export function readScalarState(memory: WebAssembly.Memory, varNames: string[]): Record<string, number> {
-  const view = new DataView(memory.buffer);
-  const result: Record<string, number> = {};
-  let offset = 0;
-
-  for (const name of varNames) {
-    // All current scalars are i32 in TigerBeetle; extend for f64 later
-    result[name] = view.getInt32(offset, true);
-    offset += 4;
-  }
-
-  return result;
-}
-
-/**
- * High-level helper: instantiate a Speckl WASM module from WAT text.
- * Requires `wat2wasm` or a WAT parser. For now, expects pre-compiled .wasm bytes.
- */
-export async function instantiateSpeckl(
-  wasmBytes: BufferSource,
-  varNames: string[]
-): Promise<{
-  exports: WebAssembly.Exports;
-  state: HostState;
-  getScalarState: () => Record<string, number>;
-}> {
-  const hostState = createHostState();
-  const imports = { speckl: createHostImports(hostState) };
-
-  const wasm = await WebAssembly.instantiate(wasmBytes, imports);
-  const memory = wasm.instance.exports.memory as WebAssembly.Memory;
-  bindMemory(hostState, memory);
-
-  const getScalarState = () => readScalarState(memory, varNames);
-
-  return {
-    exports: wasm.instance.exports,
-    state: hostState,
-    getScalarState,
-  };
-}
diff --git a/compiler/test-output/RetryHandler.prov.jsonld b/compiler/test-output/RetryHandler.prov.jsonld
index e99a4da..8da41bd 100644
--- a/compiler/test-output/RetryHandler.prov.jsonld
+++ b/compiler/test-output/RetryHandler.prov.jsonld
@@ -12,7 +12,7 @@
         "@type": "prov:Generation",
         "prov:activity": {
           "@type": "prov:Activity",
-          "prov:startTime": "2026-05-05T10:11:33.422Z"
+          "prov:startTime": "2026-05-10T05:02:58.864Z"
         }
       },
       "rdfs:label": "RetryHandler",
diff --git a/compiler/test-output/RetryHandler.specbom.cdx.json b/compiler/test-output/RetryHandler.specbom.cdx.json
index 4216014..d661bdd 100644
--- a/compiler/test-output/RetryHandler.specbom.cdx.json
+++ b/compiler/test-output/RetryHandler.specbom.cdx.json
@@ -38,7 +38,7 @@
         "name": "Scott Scoble",
         "email": "scott@scoble.me"
       },
-      "timestamp": "2026-05-05T10:11:33.425Z"
+      "timestamp": "2026-05-10T05:02:58.867Z"
     },
     {
       "subject": "speck:RetryHandler",
@@ -53,7 +53,7 @@
         "name": "Speckl Compiler",
         "email": "compiler@speckl.scoble.me"
       },
-      "timestamp": "2026-05-05T10:11:33.425Z"
+      "timestamp": "2026-05-10T05:02:58.867Z"
     },
     {
       "subject": "speck:RetryHandler",
@@ -68,7 +68,7 @@
         "name": "Speckl Compiler",
         "email": "compiler@speckl.scoble.me"
       },
-      "timestamp": "2026-05-05T10:11:33.425Z"
+      "timestamp": "2026-05-10T05:02:58.867Z"
     }
   ]
 }
\ No newline at end of file
diff --git a/compiler/test-output/RetryHandler.specbom.spdx.json b/compiler/test-output/RetryHandler.specbom.spdx.json
index 81b791e..7e5cde6 100644
--- a/compiler/test-output/RetryHandler.specbom.spdx.json
+++ b/compiler/test-output/RetryHandler.specbom.spdx.json
@@ -13,7 +13,7 @@
     "spdxVersion": "3.0.1",
     "dataLicense": "CC0-1.0",
     "creationInfo": {
-      "created": "2026-05-05T10:11:33.426Z",
+      "created": "2026-05-10T05:02:58.868Z",
       "createdBy": [
         "Organization: Speckl",
         "tool: speckl-compile-0.2.0"
@@ -27,7 +27,7 @@
           "@type": "spdx:Tool",
           "name": "speckl-compile"
         },
-        "timestamp": "2026-05-05T10:11:33.426Z",
+        "timestamp": "2026-05-10T05:02:58.868Z",
         "comment": "Review type: manual"
       }
     ]
diff --git a/examples/Paxos.speck b/examples/Paxos.speck
new file mode 100644
index 0000000..67dfe2d
--- /dev/null
+++ b/examples/Paxos.speck
@@ -0,0 +1,131 @@
+speck Paxos {
+    // Classic Paxos consensus protocol ported from TLA+ to SpeckDL v0.3
+    // Demonstrates multi-role state machines, ballot numbers, quorums,
+    // and safety invariants (at most one value chosen per slot).
+    // Adapted from Lamport's "The Part-Time Parliament" and TLA+ Paxos spec.
+
+    state {
+        // Ballot number → (value, proposer) — for each slot
+        ballots: Map(Ballot, Proposal)
+
+        // Acceptor state: which ballot each acceptor has promised for each slot
+        promises: Map(AcceptorSlot, Ballot)
+
+        // Acceptor state: last vote cast (if any) for each slot
+        lastVote: Map(AcceptorSlot, Ballot)
+
+        // Value voted for (if any) for each slot
+        votedValue: Map(AcceptorSlot, String)
+
+        // Set of acceptors
+        acceptors: Set(String)
+
+        // Quorum size (simple majority)
+        quorum: Map(String, Set(String))
+
+        // Chosen values: ballot → value (finalized)
+        chosen: Map(Ballot, String)
+    }
+
+    init {
+        let q := {"a1", "a2", "a3"}
+
+        acceptors == q
+        ballots == emptyMap
+        promises == emptyMap
+        lastVote == emptyMap
+        votedValue == emptyMap
+        chosen == emptyMap
+        quorum == emptyMap
+    }
+
+    invariant BallotUniqueness {
+        forall b in ballots.keys:
+            forall b2 in ballots.keys \ {b}:
+                b.number != b2.number
+    }
+
+    // Safety: at most one value per ballot
+    invariant SingleValuePerBallot {
+        forall b in ballots.keys:
+            forall b2 in ballots.keys:
+                b.number == b2.number implies ballots[b].value == ballots[b2].value
+    }
+
+    // Safety: if a value is chosen, no other value for that ballot
+    invariant PaxosSafety {
+        forall b in chosen.keys:
+            forall b2 in ballots.keys:
+                b2.number == b.number implies ballots[b2].value == chosen[b]
+    }
+
+    // Phase 1a: Proposer sends Prepare with ballot number
+    action ProposerPrepare(prop: String, bnum: Nat) {
+        require bnum > 0
+
+        let b := { number: bnum, value: null, proposer: prop }
+        ballots[b] := { number: bnum, value: null, proposer: prop }
+        emit PrepareSent { ballot: bnum, proposer: prop }
+    }
+
+    // Phase 1b: Acceptor receives Prepare, promises if ballot > last promised
+    action AcceptorPromise(acc: String, ballot: Nat) {
+        require acc in acceptors
+
+        let acSlot := { acceptor: acc, slot: 1 }
+        let curPromise := if acSlot in promises.keys: promises[acSlot].number else 0
+
+        require ballot > curPromise
+
+        promises[acSlot] := { number: ballot, value: null, proposer: null }
+
+        let prevVote := if acSlot in lastVote.keys: lastVote[acSlot] else { number: 0, value: null, proposer: null }
+        emit PromiseSent {
+            acceptor: acc,
+            ballot: ballot,
+            lastVoteBallot: prevVote.number,
+            lastVoteValue: if prevVote.number > 0: votedValue[acSlot] else null
+        }
+    }
+
+    // Phase 2a: Proposer collects quorum of promises, proposes value
+    action ProposerPropose(prop: String, ballot: Nat, value: String) {
+        require ballots[{ number: ballot, value: null, proposer: prop }] != null
+        require ballots[{ number: ballot, value: null, proposer: prop }].proposer == prop
+
+        ballots[{ number: ballot, value: null, proposer: prop }] :=
+            { number: ballot, value: value, proposer: prop }
+        emit ProposalSent { ballot: ballot, value: value, proposer: prop }
+    }
+
+    // Phase 2b: Acceptor votes for proposal if ballot >= last promised
+    action AcceptorVote(acc: String, ballot: Nat, value: String) {
+        require acc in acceptors
+
+        let acSlot := { acceptor: acc, slot: 1 }
+        require acSlot in promises.keys
+        require promises[acSlot].number == ballot
+
+        let prevVote := if acSlot in lastVote.keys: lastVote[acSlot].number else 0
+        require ballot >= prevVote
+
+        lastVote[acSlot] := { number: ballot, value: value, proposer: null }
+        votedValue[acSlot] := value
+        emit VotedSent { acceptor: acc, ballot: ballot, value: value }
+    }
+
+    // Learn: value is chosen when a quorum of acceptors has voted
+    action LearnerDecide(ballot: Nat, value: String) {
+        require { number: ballot, value: value, proposer: null } notIn chosen.keys
+
+        chosen[{ number: ballot, value: value, proposer: null }] := value
+        emit Chosen { ballot: ballot, value: value }
+    }
+
+    next:
+        ProposerPrepare
+        | AcceptorPromise
+        | ProposerPropose
+        | AcceptorVote
+        | LearnerDecide
+}
diff --git a/examples/PreconditionTest.speck b/examples/PreconditionTest.speck
new file mode 100644
index 0000000..e4d4c6e
--- /dev/null
+++ b/examples/PreconditionTest.speck
@@ -0,0 +1,22 @@
+speck PreconditionTest {
+
+state: {
+  balance: Integer
+  active: Boolean
+}
+
+action SetBalance(newBalance: Integer) {
+  precondition: newBalance >= 0
+  postcondition: this.balance == newBalance
+  require newBalance >= 0
+  this.balance := newBalance
+}
+
+action Deactivate() {
+  precondition: this.balance == 0
+  or this.active == false
+  postcondition: this.active == false
+  this.active := false
+}
+
+}
diff --git a/examples/Raft.speck b/examples/Raft.speck
new file mode 100644
index 0000000..7722b70
--- /dev/null
+++ b/examples/Raft.speck
@@ -0,0 +1,272 @@
+speck Raft {
+    // Raft consensus protocol ported to SpeckDL v0.3
+    // Demonstrates leader election, log replication, commitment, and safety.
+    // Based on Ongaro & Ousterhout's "In Search of an Understandable Consensus Algorithm" (2014).
+    // Natural bridge from Paxos (academic) → TigerBeetle (production replicated state machine).
+
+    type LogIndex = Nat
+    type Term = Nat
+    type ServerId = String
+
+    type LogEntry = {
+        term: Term,
+        index: LogIndex,
+        command: String
+    }
+
+    type ServerState = {
+        role: String,        // "follower", "candidate", "leader"
+        currentTerm: Term,
+        votedFor: String | null,
+        log: List(LogEntry),
+        commitIndex: LogIndex,
+        lastApplied: LogIndex
+    }
+
+    type AppendEntriesReq = {
+        term: Term,
+        leaderId: ServerId,
+        prevLogIndex: LogIndex,
+        prevLogTerm: Term,
+        entries: List(LogEntry),
+        leaderCommit: LogIndex
+    }
+
+    type RequestVoteReq = {
+        term: Term,
+        candidateId: ServerId,
+        lastLogIndex: LogIndex,
+        lastLogTerm: Term
+    }
+
+    state {
+        servers: Set(ServerId)
+        serverState: Map(ServerId, ServerState)
+
+        // Leader-specific: for each server, track nextIndex and matchIndex
+        nextIndex: Map(Map(ServerId, ServerId), LogIndex)
+        matchIndex: Map(Map(ServerId, ServerId), LogIndex)
+
+        // Election timer (abstracted as random timeout)
+        electionTimeout: Map(ServerId, Nat)
+    }
+
+    init {
+        servers == {"s1", "s2", "s3", "s4", "s5"}
+
+        // All servers start as followers in term 0
+        forall s in servers:
+            serverState[s] == {
+                role: "follower",
+                currentTerm: 0,
+                votedFor: null,
+                log: List.empty,
+                commitIndex: 0,
+                lastApplied: 0
+            }
+
+        nextIndex == emptyMap
+        matchIndex == emptyMap
+        electionTimeout == emptyMap
+    }
+
+    // Safety: Election Safety — at most one leader per term
+    invariant SingleLeaderPerTerm {
+        forall s1 in servers:
+            forall s2 in servers:
+                serverState[s1].role == "leader" and
+                serverState[s2].role == "leader" and
+                s1 != s2 implies
+                    serverState[s1].currentTerm != serverState[s2].currentTerm
+    }
+
+    // Safety: Leader Completeness — committed entries survive elections
+    invariant LeaderCompleteness {
+        forall s in servers:
+            serverState[s].role == "leader" implies
+                forall entry in serverState[s].log:
+                    entry.index <= serverState[s].commitIndex implies
+                        entry.term <= serverState[s].currentTerm
+    }
+
+    // Safety: Log Matching — if two logs have same term at same index, entries match
+    invariant LogMatching {
+        forall s1 in servers:
+            forall s2 in servers:
+                forall i in [1 .. length(serverState[s1].log)]:
+                    i <= length(serverState[s2].log) and
+                    serverState[s1].log[i].term == serverState[s2].log[i].term implies
+                        serverState[s1].log[i].command == serverState[s2].log[i].command
+    }
+
+    // Start election: follower times out, becomes candidate
+    action StartElection(server: ServerId) {
+        require server in servers
+        require serverState[server].role == "follower"
+
+        let newTerm := serverState[server].currentTerm + 1
+
+        // Increment term, vote for self
+        serverState[server].currentTerm := newTerm
+        serverState[server].role := "candidate"
+        serverState[server].votedFor := server
+
+        emit ElectionStarted { server: server, term: newTerm }
+    }
+
+    // Grant vote: follower votes for candidate if candidate's log is at least as up-to-date
+    action GrantVote(voter: ServerId, req: RequestVoteReq) {
+        require voter in servers
+        require serverState[voter].role == "follower" or
+                serverState[voter].role == "candidate"
+
+        // Only vote if candidate's term >= our term
+        require req.term >= serverState[voter].currentTerm
+
+        // If candidate's term > ours, step down
+        if req.term > serverState[voter].currentTerm {
+            serverState[voter].currentTerm := req.term
+            serverState[voter].role := "follower"
+            serverState[voter].votedFor := null
+        }
+
+        // Check not already voted in this term
+        require serverState[voter].votedFor == null or
+                serverState[voter].votedFor == req.candidateId
+
+        // Candidate log must be at least as complete as ours
+        let voterLog := serverState[voter].log
+        let voterLastIndex := length(voterLog)
+        let voterLastTerm := if voterLastIndex > 0: voterLog[voterLastIndex].term else 0
+
+        require req.lastLogTerm > voterLastTerm or
+                (req.lastLogTerm == voterLastTerm and req.lastLogIndex >= voterLastIndex)
+
+        serverState[voter].votedFor := req.candidateId
+        emit VoteGranted { voter: voter, candidate: req.candidateId, term: req.term }
+    }
+
+    // Become leader: candidate receives majority of votes
+    action BecomeLeader(server: ServerId) {
+        require server in servers
+        require serverState[server].role == "candidate"
+
+        // Count votes received (simplified: assumes quorum reached via external counting)
+        serverState[server].role := "leader"
+
+        // Initialize nextIndex/matchIndex for all other servers
+        forall s in servers \ {server}:
+            let lastLogIndex := length(serverState[server].log)
+            nextIndex[{ leader: server, follower: s }] := lastLogIndex + 1
+            matchIndex[{ leader: server, follower: s }] := 0
+
+        emit LeaderElected { leader: server, term: serverState[server].currentTerm }
+
+        // Send initial empty AppendEntries (heartbeat) to assert leadership
+        emit HeartbeatSent { leader: server, term: serverState[server].currentTerm }
+    }
+
+    // Append entries: leader replicates log entry to followers
+    action AppendEntries(leader: ServerId, follower: ServerId, req: AppendEntriesReq) {
+        require leader in servers
+        require follower in servers
+        require leader != follower
+        require serverState[leader].role == "leader"
+
+        // Verify term consistency
+        let followerTerm := serverState[follower].currentTerm
+        require req.term >= followerTerm
+
+        // If leader's term is stale, step down
+        if req.term > serverState[leader].currentTerm {
+            serverState[leader].currentTerm := req.term
+            serverState[leader].role := "follower"
+            serverState[leader].votedFor := null
+            return
+        }
+
+        // Update follower's term if behind
+        if req.term > followerTerm {
+            serverState[follower].currentTerm := req.term
+            serverState[follower].role := "follower"
+            serverState[follower].votedFor := null
+        }
+
+        // Check log consistency at prevLogIndex
+        let fLog := serverState[follower].log
+        require req.prevLogIndex == 0 or
+                (req.prevLogIndex <= length(fLog) and
+                 fLog[req.prevLogIndex].term == req.prevLogTerm)
+
+        // Delete conflicting entries, append new ones
+        let truncated := if req.prevLogIndex < length(fLog):
+                            take(fLog, req.prevLogIndex)
+                        else fLog
+
+        serverState[follower].log := concat(truncated, req.entries)
+
+        // Update commit index
+        if req.leaderCommit > serverState[follower].commitIndex {
+            let lastNewEntry := req.prevLogIndex + length(req.entries)
+            serverState[follower].commitIndex :=
+                if req.leaderCommit < lastNewEntry: req.leaderCommit else lastNewEntry
+        }
+
+        emit EntriesReplicated {
+            leader: leader,
+            follower: follower,
+            entries: length(req.entries)
+        }
+    }
+
+    // Advance commit index: leader commits when majority replicated
+    action AdvanceCommit(leader: ServerId) {
+        require leader in servers
+        require serverState[leader].role == "leader"
+
+        let currentCommit := serverState[leader].commitIndex
+        let logLen := length(serverState[leader].log)
+
+        // Find highest index that has been replicated to a majority
+        for i from currentCommit + 1 to logLen:
+            let replicated := 1  // leader counts itself
+            forall s in servers \ {leader}:
+                if matchIndex[{ leader: leader, follower: s }] >= i:
+                    replicated := replicated + 1
+
+            if replicated * 2 > size(servers) and
+               serverState[leader].log[i].term == serverState[leader].currentTerm {
+                serverState[leader].commitIndex := i
+            }
+
+        emit CommitAdvanced {
+            leader: leader,
+            commitIndex: serverState[leader].commitIndex
+        }
+    }
+
+    // Apply committed entries to state machine
+    action ApplyEntries(server: ServerId) {
+        require server in servers
+
+        let s := serverState[server]
+        let commitIdx := s.commitIndex
+
+        for i from s.lastApplied + 1 to commitIdx:
+            emit CommandApplied {
+                server: server,
+                index: i,
+                command: s.log[i].command
+            }
+
+        serverState[server].lastApplied := commitIdx
+    }
+
+    next:
+        StartElection
+        | GrantVote
+        | BecomeLeader
+        | AppendEntries
+        | AdvanceCommit
+        | ApplyEntries
+}
\ No newline at end of file
diff --git a/reference-agent/src/types.ts b/reference-agent/src/types.ts
index 7c09802..0877789 100644
--- a/reference-agent/src/types.ts
+++ b/reference-agent/src/types.ts
@@ -99,7 +99,7 @@ export interface Task {
 export type TaskType = 
   | "verify_speck"      // Run Z3 verification on a Speck
   | "compile_to_dst"    // Compile verified Speck to DST
-  | "compile_to_wasm"   // Compile DST to WASM
+  | "compile_to_wasm  // Removed: WASM superseded by IR→Rust→wasm-pack path
   | "generate_code"     // Generate code from verified Speck
   | "generate_docs"     // Generate documentation from provenance graph
   | "integrate"         // Integration/glue code