diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 2e29aad..9e85c4a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -39,7 +39,11 @@ jobs:
           timeout 60 node -e "require('./dist/node.js').createDemo().createIdentity()"
       - name: Audit runtime dependencies
         run: npm audit --omit=dev --audit-level=high
-      - run: npm pack --dry-run --ignore-scripts
+      - name: Pack, install the tarball into a temp project, check every entry point and MCP stdio
+        run: |
+          npm pack --ignore-scripts --pack-destination "$RUNNER_TEMP"
+          version=$(node -p "require('./package.json').version")
+          timeout 600 node scripts/check-package.mjs "$RUNNER_TEMP/lean-agentic-$version.tgz"
 
   rust:
     name: cargo test
diff --git a/leanr-wasm/src/lib.rs b/leanr-wasm/src/lib.rs
index f3e311c..82cd0fe 100644
--- a/leanr-wasm/src/lib.rs
+++ b/leanr-wasm/src/lib.rs
@@ -7,8 +7,26 @@ use lean_agentic::{Arena, Environment, SymbolTable};
 use lean_agentic::level::LevelArena;
 use lean_agentic::term::{Binder, BinderInfo};
 use wasm_bindgen::prelude::*;
+use std::sync::atomic::{AtomicBool, Ordering};
 use web_sys::console;
 
+/// Diagnostic logging is off by default. When on, it goes to `console.error`
+/// (stderr under Node), so it never mixes with stdout, which the MCP server
+/// uses for JSON-RPC.
+static DEBUG: AtomicBool = AtomicBool::new(false);
+
+fn debug_log(msg: &str) {
+    if DEBUG.load(Ordering::Relaxed) {
+        console::error_1(&msg.into());
+    }
+}
+
+/// Turn diagnostic logging on or off (off by default).
+#[wasm_bindgen(js_name = setDebug)]
+pub fn set_debug(enabled: bool) {
+    DEBUG.store(enabled, Ordering::Relaxed);
+}
+
 /// Demo struct showing hash-consing performance in WASM
 #[wasm_bindgen]
 pub struct LeanDemo {
@@ -24,7 +42,7 @@ impl LeanDemo {
     /// Create a new Lean demo instance
     #[wasm_bindgen(constructor)]
     pub fn new() -> Self {
-        console::log_1(&"Initializing Lean-Agentic WASM...".into());
+        debug_log("Initializing Lean-Agentic WASM...");
 
         Self {
             arena: Arena::new(),
@@ -41,7 +59,7 @@ impl LeanDemo {
     pub fn create_variable(&mut self, index: u32) -> bool {
         let term = self.arena.mk_var(index);
         self.term_counter += 1;
-        console::log_1(&format!("Created variable with index {} -> TermId {:?}", index, term).into());
+        debug_log(&format!("Created variable with index {} -> TermId {:?}", index, term));
         true
     }
 
@@ -54,10 +72,10 @@ impl LeanDemo {
 
         let same = var1 == var2;
 
-        console::log_1(&format!(
+        debug_log(&format!(
             "Hash-consing test: var1={:?}, var2={:?}, same={}",
             var1, var2, same
-        ).into());
+        ));
 
         same
     }
@@ -77,7 +95,7 @@ impl LeanDemo {
         let level_zero = self.levels.zero();
         let type_term = self.arena.mk_sort(level_zero);
         self.term_counter += 1;
-        console::log_1(&format!("Created Type: {:?}", type_term).into());
+        debug_log(&format!("Created Type: {:?}", type_term));
         true
     }
 
@@ -100,7 +118,7 @@ impl LeanDemo {
         let lambda = self.arena.mk_lam(binder, var_x);
 
         self.term_counter += 3;
-        console::log_1(&format!("Created identity function: λx:Type. x = {:?}", lambda).into());
+        debug_log(&format!("Created identity function: λx:Type. x = {:?}", lambda));
         true
     }
 
diff --git a/npm/lean-agentic/README.md b/npm/lean-agentic/README.md
index 0b7a06d..296894b 100644
--- a/npm/lean-agentic/README.md
+++ b/npm/lean-agentic/README.md
@@ -549,7 +549,11 @@ demo.createApplication();
 demo.demonstrateHashConsing();
 ```
 
-### Bundler API
+### Root entry point (Node.js)
+
+The root entry point is the Node.js build (same API as `lean-agentic/node`, plus `init()`). In the browser, use `lean-agentic/web`.
+
+The WASM module is silent by default. Set `LEAN_AGENTIC_DEBUG=1` (or call `setDebug(true)`) to print its diagnostic logs; they go to stderr, so they never mix with the MCP server's JSON-RPC on stdout.
 
 ```javascript
 import { init, createDemo } from 'lean-agentic';
@@ -610,11 +614,9 @@ console.timeEnd('Hash-consed equality');
 
 | Platform | Support | Import |
 |----------|---------|--------|
-| Node.js 18+ | ✅ | `lean-agentic/node` |
+| Node.js 18+ | ✅ | `lean-agentic` or `lean-agentic/node` |
 | Browser (ESM) | ✅ | `lean-agentic/web` |
-| Webpack | ✅ | `lean-agentic` |
-| Vite | ✅ | `lean-agentic` |
-| Rollup | ✅ | `lean-agentic` |
+| Webpack / Vite / Rollup (browser) | ✅ | `lean-agentic/web` |
 | Deno | ✅ | `npm:lean-agentic` |
 | Bun | ✅ | `lean-agentic` |
 
@@ -671,7 +673,6 @@ cd lean-agentic
 cd leanr-wasm
 wasm-pack build --target nodejs --out-dir ../npm/lean-agentic/wasm-node
 wasm-pack build --target web --out-dir ../npm/lean-agentic/wasm-web
-wasm-pack build --target bundler --out-dir ../npm/lean-agentic/wasm
 
 # Install dependencies
 cd ../npm/lean-agentic
diff --git a/npm/lean-agentic/cli/index.js b/npm/lean-agentic/cli/index.js
index 4c8262e..7f66095 100755
--- a/npm/lean-agentic/cli/index.js
+++ b/npm/lean-agentic/cli/index.js
@@ -164,9 +164,13 @@ mcp
     console.error('Tools: 5 | Resources: 2 | Prompts: 2');
     console.error('Ready for Claude Code integration\n');
 
-    // Launch the MCP server
+    // Launch the MCP server. Requiring server.js alone does not start it
+    // (it only auto-starts when run directly), so call startServer().
     const serverPath = join(__dirname, '../mcp/server.js');
-    require(serverPath);
+    require(serverPath).startServer().catch((error) => {
+      process.stderr.write(`Fatal error: ${error}\n`);
+      process.exit(1);
+    });
   });
 
 mcp
diff --git a/npm/lean-agentic/dist/index.d.ts b/npm/lean-agentic/dist/index.d.ts
index a5aa192..7586efa 100644
--- a/npm/lean-agentic/dist/index.d.ts
+++ b/npm/lean-agentic/dist/index.d.ts
@@ -1,73 +1,31 @@
 /**
  * lean-agentic TypeScript definitions
  *
- * Hash-consed dependent types with 150x faster equality
+ * Hash-consed dependent types with 150x faster equality. Under Node.js the
+ * root entry point has the same API as `lean-agentic/node`, plus `init()`.
+ * Browsers should use `lean-agentic/web`.
  *
  * @module lean-agentic
  * @author ruv.io
  * @license Apache-2.0
  */
 
-/**
- * Initialize the WASM module
- */
-export function init(): Promise<void>;
+import { LeanDemo, createDemo, quickStart, setDebug, wasm } from './node';
 
-/**
- * Main interface for lean-agentic theorem prover
- */
-export class LeanDemo {
-  constructor();
-
-  /**
-   * Create identity function: λx:Type. x
-   * @returns JSON representation of the identity function
-   */
-  createIdentity(): string;
-
-  /**
-   * Create and verify an application
-   * @returns JSON representation of the application
-   */
-  createApplication(): string;
-
-  /**
-   * Demonstrate hash-consing by creating identical terms
-   * @returns JSON showing term equality
-   */
-  demonstrateHashConsing(): string;
-}
+export { LeanDemo, createDemo, quickStart, setDebug, wasm };
 
 /**
- * Create a new LeanDemo instance
+ * Kept for API compatibility. Resolves immediately: the Node WASM build is
+ * ready as soon as it is loaded.
  */
-export function createDemo(): LeanDemo;
-
-/**
- * Quick start: Create identity function
- */
-export function quickStart(): Promise<string>;
-
-/**
- * WASM module exports
- */
-export namespace wasm {
-  export class LeanDemo {
-    constructor();
-    create_identity(): string;
-    create_application(): string;
-    demonstrate_hash_consing(): string;
-  }
-}
+export function init(): Promise<void>;
 
-/**
- * Default export
- */
 declare const _default: {
   init: typeof init;
   LeanDemo: typeof LeanDemo;
   createDemo: typeof createDemo;
   quickStart: typeof quickStart;
+  setDebug: typeof setDebug;
   wasm: typeof wasm;
 };
 
diff --git a/npm/lean-agentic/dist/index.js b/npm/lean-agentic/dist/index.js
index bbb626e..c94e0b2 100644
--- a/npm/lean-agentic/dist/index.js
+++ b/npm/lean-agentic/dist/index.js
@@ -1,81 +1,29 @@
 /**
  * lean-agentic - Hash-consed dependent types with 150x faster equality
  *
+ * Root entry point. Under Node.js this is the same API as `lean-agentic/node`,
+ * plus an `init()` that resolves immediately (the Node WASM build loads
+ * synchronously). Browsers should use `lean-agentic/web`.
+ *
  * @module lean-agentic
  * @author ruv.io
  * @license Apache-2.0
  */
 
-const wasm = require('../wasm/leanr_wasm.js');
+const node = require('./node.js');
 
 /**
- * Initialize the WASM module
+ * Kept for API compatibility: the Node WASM build is ready as soon as it is
+ * required, so there is nothing to wait for.
  * @returns {Promise<void>}
  */
-export async function init() {
-  // WASM is already initialized when imported
-  return Promise.resolve();
-}
-
-/**
- * LeanDemo - Main interface for lean-agentic
- */
-class LeanDemo {
-  constructor() {
-    this._inner = new wasm.LeanDemo();
-  }
-
-  /**
-   * Create identity function: λx:Type. x
-   * @returns {string} JSON representation of the identity function
-   */
-  createIdentity() {
-    return this._inner.create_identity();
-  }
-
-  /**
-   * Create and verify an application
-   * @returns {string} JSON representation of the application
-   */
-  createApplication() {
-    return this._inner.create_application();
-  }
-
-  /**
-   * Demonstrate hash-consing by creating identical terms
-   * @returns {string} JSON showing term equality
-   */
-  demonstrateHashConsing() {
-    return this._inner.demonstrate_hash_consing();
-  }
-}
-
-/**
- * Create a new LeanDemo instance
- * @returns {LeanDemo}
- */
-function createDemo() {
-  return new LeanDemo();
-}
-
-/**
- * Quick start: Create identity function
- * @returns {Promise<string>}
- */
-export async function quickStart() {
-  await init();
-  const demo = createDemo();
-  return demo.createIdentity();
-}
-
-// Re-export WASM types
-module.exports = { wasm };
+async function init() {}
 
-// Default export
 module.exports = {
   init,
-  LeanDemo,
-  createDemo,
-  quickStart,
-  wasm
+  LeanDemo: node.LeanDemo,
+  createDemo: node.createDemo,
+  quickStart: node.quickStart,
+  setDebug: node.setDebug,
+  wasm: node.wasm
 };
diff --git a/npm/lean-agentic/dist/index.mjs b/npm/lean-agentic/dist/index.mjs
index 9eec57c..70fcbea 100644
--- a/npm/lean-agentic/dist/index.mjs
+++ b/npm/lean-agentic/dist/index.mjs
@@ -1,81 +1,8 @@
-/**
- * lean-agentic - Hash-consed dependent types with 150x faster equality
- *
- * @module lean-agentic
- * @author ruv.io
- * @license Apache-2.0
- */
+// Generated by scripts/build.js. Do not edit.
+import { createRequire } from 'node:module';
 
-import * as wasm from '../wasm/leanr_wasm.js';
+const require = createRequire(import.meta.url);
+const mod = require('./index.js');
 
-/**
- * Initialize the WASM module
- * @returns {Promise<void>}
- */
-export async function init() {
-  // WASM is already initialized when imported
-  return Promise.resolve();
-}
-
-/**
- * LeanDemo - Main interface for lean-agentic
- */
-export class LeanDemo {
-  constructor() {
-    this._inner = new wasm.LeanDemo();
-  }
-
-  /**
-   * Create identity function: λx:Type. x
-   * @returns {string} JSON representation of the identity function
-   */
-  createIdentity() {
-    return this._inner.create_identity();
-  }
-
-  /**
-   * Create and verify an application
-   * @returns {string} JSON representation of the application
-   */
-  createApplication() {
-    return this._inner.create_application();
-  }
-
-  /**
-   * Demonstrate hash-consing by creating identical terms
-   * @returns {string} JSON showing term equality
-   */
-  demonstrateHashConsing() {
-    return this._inner.demonstrate_hash_consing();
-  }
-}
-
-/**
- * Create a new LeanDemo instance
- * @returns {LeanDemo}
- */
-export function createDemo() {
-  return new LeanDemo();
-}
-
-/**
- * Quick start: Create identity function
- * @returns {Promise<string>}
- */
-export async function quickStart() {
-  await init();
-  const demo = createDemo();
-  return demo.createIdentity();
-}
-
-// Re-export WASM types
-export { wasm };
-
-// Default export
-export default {
-  init,
-  LeanDemo,
-  createDemo,
-  quickStart,
-  wasm
-};
+export const { LeanDemo, createDemo, init, quickStart, setDebug, wasm } = mod;
+export default mod;
diff --git a/npm/lean-agentic/dist/node.d.ts b/npm/lean-agentic/dist/node.d.ts
index 2eb7904..35db556 100644
--- a/npm/lean-agentic/dist/node.d.ts
+++ b/npm/lean-agentic/dist/node.d.ts
@@ -12,19 +12,48 @@
  */
 export class LeanDemo {
   constructor();
+  /** JSON describing the identity function λx:Type. x */
   createIdentity(): string;
+  /** JSON describing an application (var0 var1) */
   createApplication(): string;
+  /** JSON showing that identical terms share one TermId */
   demonstrateHashConsing(): string;
+  /** JSON with arena statistics */
+  getStats(): string;
+  benchmarkEquality(): string;
 }
 
 export function createDemo(): LeanDemo;
 export function quickStart(): Promise<string>;
 
-export namespace wasm {
-  export class LeanDemo {
-    constructor();
-    create_identity(): string;
-    create_application(): string;
-    demonstrate_hash_consing(): string;
-  }
-}
+/**
+ * Turn the WASM module's diagnostic logging on or off. Logs go to stderr.
+ * Off by default; LEAN_AGENTIC_DEBUG=1 turns it on at load time.
+ */
+export function setDebug(enabled: boolean): void;
+
+/** Raw wasm-bindgen module (types: wasm-node/leanr_wasm.d.ts) */
+export const wasm: {
+  LeanDemo: new () => {
+    free(): void;
+    createVariable(index: number): boolean;
+    demonstrateHashConsing(): boolean;
+    getStats(): string;
+    createType(): boolean;
+    createIdentityFunction(): boolean;
+    benchmarkEquality(): string;
+  };
+  greet(name: string): string;
+  getVersion(): string;
+  setDebug(enabled: boolean): void;
+};
+
+declare const _default: {
+  LeanDemo: typeof LeanDemo;
+  createDemo: typeof createDemo;
+  quickStart: typeof quickStart;
+  setDebug: typeof setDebug;
+  wasm: typeof wasm;
+};
+
+export default _default;
diff --git a/npm/lean-agentic/dist/node.js b/npm/lean-agentic/dist/node.js
index 535c5b7..3c03817 100644
--- a/npm/lean-agentic/dist/node.js
+++ b/npm/lean-agentic/dist/node.js
@@ -8,6 +8,19 @@
 
 const wasm = require('../wasm-node/leanr_wasm.js');
 
+/**
+ * Turn the WASM module's diagnostic logging on or off. Logs go to stderr
+ * (console.error), never stdout. Off by default; set LEAN_AGENTIC_DEBUG=1
+ * to turn it on at load time.
+ * @param {boolean} enabled
+ */
+function setDebug(enabled) {
+  wasm.setDebug(Boolean(enabled));
+}
+
+const debugEnv = process.env.LEAN_AGENTIC_DEBUG;
+setDebug(debugEnv !== undefined && debugEnv !== '' && debugEnv !== '0' && debugEnv !== 'false');
+
 /**
  * LeanDemo - Node.js interface
  */
@@ -78,5 +91,6 @@ module.exports = {
   LeanDemo,
   createDemo,
   quickStart,
+  setDebug,
   wasm
 };
diff --git a/npm/lean-agentic/dist/node.mjs b/npm/lean-agentic/dist/node.mjs
index 535c5b7..5fe085e 100644
--- a/npm/lean-agentic/dist/node.mjs
+++ b/npm/lean-agentic/dist/node.mjs
@@ -1,82 +1,8 @@
-/**
- * lean-agentic/node - Node.js-specific bindings
- *
- * @module lean-agentic/node
- * @author ruv.io
- * @license Apache-2.0
- */
+// Generated by scripts/build.js. Do not edit.
+import { createRequire } from 'node:module';
 
-const wasm = require('../wasm-node/leanr_wasm.js');
+const require = createRequire(import.meta.url);
+const mod = require('./node.js');
 
-/**
- * LeanDemo - Node.js interface
- */
-class LeanDemo {
-  constructor() {
-    this._inner = new wasm.LeanDemo();
-  }
-
-  createIdentity() {
-    this._inner.createIdentityFunction();
-    return JSON.stringify({
-      term: "Lambda",
-      description: "λx:Type. x (identity function)",
-      note: "Hash-consed for O(1) equality"
-    });
-  }
-
-  createApplication() {
-    this._inner.createVariable(0);
-    this._inner.createVariable(1);
-    return JSON.stringify({
-      term: "Application",
-      description: "(var0 var1)",
-      note: "Zero-copy arena allocation"
-    });
-  }
-
-  demonstrateHashConsing() {
-    const result = this._inner.demonstrateHashConsing();
-    return JSON.stringify({
-      demo: "Hash-Consing",
-      all_equal: result,
-      explanation: "Identical terms share the same TermId! Equality is O(1) pointer comparison.",
-      speedup: "150x faster than structural equality"
-    });
-  }
-
-  getStats() {
-    const stats = this._inner.getStats();
-    // Parse the stats string into JSON format
-    // Format: "Arena operations: N (hash-consed for 150x faster equality)"
-    const match = stats.match(/Arena operations: (\d+)/);
-    const operations = match ? parseInt(match[1]) : 0;
-
-    return JSON.stringify({
-      unique_terms: operations,
-      message: stats,
-      hash_consing_enabled: true,
-      performance_multiplier: "150x faster"
-    });
-  }
-
-  benchmarkEquality() {
-    return this._inner.benchmarkEquality();
-  }
-}
-
-function createDemo() {
-  return new LeanDemo();
-}
-
-async function quickStart() {
-  const demo = createDemo();
-  return demo.createIdentity();
-}
-
-module.exports = {
-  LeanDemo,
-  createDemo,
-  quickStart,
-  wasm
-};
+export const { LeanDemo, createDemo, quickStart, setDebug, wasm } = mod;
+export default mod;
diff --git a/npm/lean-agentic/dist/web.d.ts b/npm/lean-agentic/dist/web.d.ts
index 2ae16c9..1fc30f4 100644
--- a/npm/lean-agentic/dist/web.d.ts
+++ b/npm/lean-agentic/dist/web.d.ts
@@ -21,23 +21,39 @@ export class LeanDemo {
   createIdentity(): string;
   createApplication(): string;
   demonstrateHashConsing(): string;
+  getStats(): string;
+  benchmarkEquality(): string;
 }
 
 export function createDemo(): LeanDemo;
 
-export namespace wasm {
-  export class LeanDemo {
-    constructor();
-    create_identity(): string;
-    create_application(): string;
-    demonstrate_hash_consing(): string;
-  }
-}
+/**
+ * Turn the WASM module's diagnostic logging (console.error) on or off.
+ * Off by default. Call after initWeb().
+ */
+export function setDebug(enabled: boolean): void;
+
+/** Raw wasm-bindgen module (types: wasm-web/leanr_wasm.d.ts) */
+export const wasm: {
+  LeanDemo: new () => {
+    free(): void;
+    createVariable(index: number): boolean;
+    demonstrateHashConsing(): boolean;
+    getStats(): string;
+    createType(): boolean;
+    createIdentityFunction(): boolean;
+    benchmarkEquality(): string;
+  };
+  greet(name: string): string;
+  getVersion(): string;
+  setDebug(enabled: boolean): void;
+};
 
 declare const _default: {
   initWeb: typeof initWeb;
   LeanDemo: typeof LeanDemo;
   createDemo: typeof createDemo;
+  setDebug: typeof setDebug;
   wasm: typeof wasm;
 };
 
diff --git a/npm/lean-agentic/dist/web.mjs b/npm/lean-agentic/dist/web.mjs
index 05aa215..5920b7c 100644
--- a/npm/lean-agentic/dist/web.mjs
+++ b/npm/lean-agentic/dist/web.mjs
@@ -87,6 +87,15 @@ export class LeanDemo {
   }
 }
 
+/**
+ * Turn the WASM module's diagnostic logging (console.error) on or off.
+ * Off by default. Call after initWeb().
+ * @param {boolean} enabled
+ */
+export function setDebug(enabled) {
+  wasm.setDebug(Boolean(enabled));
+}
+
 export function createDemo() {
   return new LeanDemo();
 }
@@ -95,5 +104,6 @@ export default {
   initWeb,
   LeanDemo,
   createDemo,
+  setDebug,
   wasm
 };
diff --git a/npm/lean-agentic/mcp/server.js b/npm/lean-agentic/mcp/server.js
index 2eadf4d..4bb31a7 100755
--- a/npm/lean-agentic/mcp/server.js
+++ b/npm/lean-agentic/mcp/server.js
@@ -525,6 +525,11 @@ class LeanAgenticMCPServer {
       return;
     }
 
+    // Notifications (e.g. notifications/initialized) get no response.
+    if (id === undefined && typeof method === 'string' && method.startsWith('notifications/')) {
+      return;
+    }
+
     this.log(`Handling ${method} request`);
 
     switch (method) {
@@ -565,6 +570,13 @@ class LeanAgenticMCPServer {
    * Start the stdio server
    */
   async start() {
+    // stdout carries JSON-RPC only. Send anything that calls console.log,
+    // console.info or console.debug (dependencies included) to stderr.
+    const toStderr = (...args) => console.error(...args);
+    console.log = toStderr;
+    console.info = toStderr;
+    console.debug = toStderr;
+
     await this.initialize();
 
     const rl = readline.createInterface({
@@ -594,13 +606,20 @@ class LeanAgenticMCPServer {
   }
 }
 
+/**
+ * Start the stdio server in this process.
+ */
+function startServer() {
+  const server = new LeanAgenticMCPServer();
+  return server.start();
+}
+
 // Start the server
 if (require.main === module) {
-  const server = new LeanAgenticMCPServer();
-  server.start().catch((error) => {
+  startServer().catch((error) => {
     process.stderr.write(`Fatal error: ${error}\n`);
     process.exit(1);
   });
 }
 
-module.exports = { LeanAgenticMCPServer };
+module.exports = { LeanAgenticMCPServer, startServer };
diff --git a/npm/lean-agentic/package-lock.json b/npm/lean-agentic/package-lock.json
index 331d04a..f79443b 100644
--- a/npm/lean-agentic/package-lock.json
+++ b/npm/lean-agentic/package-lock.json
@@ -1,12 +1,12 @@
 {
   "name": "lean-agentic",
-  "version": "0.3.3",
+  "version": "0.3.4",
   "lockfileVersion": 3,
   "requires": true,
   "packages": {
     "": {
       "name": "lean-agentic",
-      "version": "0.3.3",
+      "version": "0.3.4",
       "license": "Apache-2.0",
       "dependencies": {
         "commander": "^12.0.0"
diff --git a/npm/lean-agentic/package.json b/npm/lean-agentic/package.json
index 64cdada..eeacc23 100644
--- a/npm/lean-agentic/package.json
+++ b/npm/lean-agentic/package.json
@@ -1,6 +1,6 @@
 {
   "name": "lean-agentic",
-  "version": "0.3.3",
+  "version": "0.3.4",
   "description": "High-performance WebAssembly theorem prover with dependent types, hash-consing (150x faster), Ed25519 proof signatures, MCP support for Claude Code, AgentDB vector search, episodic memory, and ReasoningBank learning. Formal verification with cryptographic attestation and AI-powered proof recommendations.",
   "main": "dist/index.js",
   "module": "dist/index.mjs",
@@ -14,21 +14,21 @@
       "import": "./dist/index.mjs",
       "require": "./dist/index.js"
     },
-    "./web": {
-      "types": "./dist/web.d.ts",
-      "import": "./dist/web.mjs"
-    },
     "./node": {
       "types": "./dist/node.d.ts",
       "import": "./dist/node.mjs",
       "require": "./dist/node.js"
-    }
+    },
+    "./web": {
+      "types": "./dist/web.d.ts",
+      "import": "./dist/web.mjs"
+    },
+    "./package.json": "./package.json"
   },
   "files": [
     "dist",
     "cli",
     "src",
-    "wasm",
     "wasm-node",
     "wasm-web",
     "mcp",
@@ -38,9 +38,9 @@
   ],
   "scripts": {
     "build": "npm run build:wasm && npm run build:js",
-    "build:wasm": "cd ../../leanr-wasm && wasm-pack build --target bundler --out-dir ../npm/lean-agentic/wasm",
+    "build:wasm": "cd ../../leanr-wasm && wasm-pack build --release --target nodejs --out-dir ../npm/lean-agentic/wasm-node && wasm-pack build --release --target web --out-dir ../npm/lean-agentic/wasm-web && rm -f ../npm/lean-agentic/wasm-node/.gitignore ../npm/lean-agentic/wasm-web/.gitignore",
     "build:js": "node scripts/build.js",
-    "prepublishOnly": "npm run build",
+    "prepublishOnly": "npm run build:js",
     "test": "node --test tests/agentdb/*.test.js tests/theorems/basic-theorems.test.js tests/theorems/dependent-types.test.js",
     "example:node": "node examples/node-example.js",
     "example:web": "npx serve examples",
diff --git a/npm/lean-agentic/scripts/build.js b/npm/lean-agentic/scripts/build.js
index 96f265b..b24ea66 100755
--- a/npm/lean-agentic/scripts/build.js
+++ b/npm/lean-agentic/scripts/build.js
@@ -1,8 +1,15 @@
 #!/usr/bin/env node
 
 /**
- * Build script for lean-agentic npm package
- * Creates both CommonJS and ESM bundles
+ * Build script for lean-agentic npm package.
+ *
+ * dist/node.js  and dist/index.js  - CommonJS, copied from src/
+ * dist/node.mjs and dist/index.mjs - ESM wrappers that load the CommonJS
+ *                                    build through createRequire, so both
+ *                                    module systems share one WASM instance
+ * dist/web.mjs                     - ESM, copied from src/
+ *
+ * Diagnostics go to stderr so `node scripts/build.js` stays quiet on stdout.
  */
 
 const fs = require('fs');
@@ -11,88 +18,39 @@ const path = require('path');
 const srcDir = path.join(__dirname, '..', 'src');
 const distDir = path.join(__dirname, '..', 'dist');
 
-// Ensure dist directory exists
-if (!fs.existsSync(distDir)) {
-  fs.mkdirSync(distDir, { recursive: true });
-}
-
-// Files to build
-const files = [
-  { name: 'index', hasCommonJS: true },
-  { name: 'node', hasCommonJS: true },
-  { name: 'web', hasCommonJS: false } // Web only needs ESM
-];
-
-console.log('📦 Building lean-agentic...\n');
-
-files.forEach(({ name, hasCommonJS }) => {
-  const srcFile = path.join(srcDir, `${name}.js`);
-
-  if (!fs.existsSync(srcFile)) {
-    console.warn(`⚠️  Warning: ${srcFile} not found, skipping...`);
-    return;
-  }
-
-  const content = fs.readFileSync(srcFile, 'utf-8');
-
-  // Create ESM version (.mjs)
-  const mjsFile = path.join(distDir, `${name}.mjs`);
-  fs.writeFileSync(mjsFile, content);
-  console.log(`✅ Created ${name}.mjs`);
-
-  // Create CommonJS version (.js) if needed
-  if (hasCommonJS) {
-    const cjsFile = path.join(distDir, `${name}.js`);
-    const cjsContent = convertToCommonJS(content, name);
-    fs.writeFileSync(cjsFile, cjsContent);
-    console.log(`✅ Created ${name}.js`);
-  }
-});
-
-console.log('\n✨ Build complete!\n');
-console.log('📁 Output:');
-console.log('  - dist/*.mjs (ES Modules)');
-console.log('  - dist/*.js  (CommonJS)');
-console.log('  - dist/*.d.ts (TypeScript definitions)\n');
+fs.mkdirSync(distDir, { recursive: true });
 
-/**
- * Convert ES Module syntax to CommonJS
- */
-function convertToCommonJS(content, moduleName) {
-  // Handle different module types
-  if (moduleName === 'node') {
-    // node.js already uses CommonJS, just copy it
-    return content;
-  }
+function copy(from, to) {
+  fs.copyFileSync(path.join(srcDir, from), path.join(distDir, to));
+  console.error(`created dist/${to}`);
+}
 
-  if (moduleName === 'web') {
-    // Web module doesn't need CommonJS
-    return content;
+function esmWrapper(cjsName) {
+  // Load the CommonJS build to learn its export names.
+  const mod = require(path.join(distDir, `${cjsName}.js`));
+  const names = Object.keys(mod).sort();
+  for (const name of names) {
+    if (!/^[A-Za-z_$][\w$]*$/.test(name) || name === 'default') {
+      throw new Error(`dist/${cjsName}.js exports an unsupported name: ${name}`);
+    }
   }
-
-  // For index.js (bundler), convert import/export to require/module.exports
-  let cjs = content
-    // Convert: import ... from '../wasm/...'
-    .replace(/import\s+(\w+|\{[^}]+\}|\*\s+as\s+\w+)\s+from\s+['"]([^'"]+)['"]/g,
-      (match, imports, path) => {
-        if (imports.startsWith('*')) {
-          const varName = imports.match(/\*\s+as\s+(\w+)/)[1];
-          return `const ${varName} = require('${path}')`;
-        } else if (imports.startsWith('{')) {
-          return `const ${imports} = require('${path}')`;
-        } else {
-          return `const ${imports} = require('${path}')`;
-        }
-      })
-    // Convert: export class/function
-    .replace(/export\s+(class|function|const|let|var)\s+(\w+)/g, '$1 $2')
-    // Convert: export default
-    .replace(/export\s+default\s+/g, 'module.exports = ')
-    // Convert: export { ... }
-    .replace(/export\s*\{([^}]+)\}/g, (match, exports) => {
-      const items = exports.split(',').map(e => e.trim());
-      return `module.exports = { ${items.join(', ')} }`;
-    });
-
-  return cjs;
+  const body = [
+    '// Generated by scripts/build.js. Do not edit.',
+    "import { createRequire } from 'node:module';",
+    '',
+    'const require = createRequire(import.meta.url);',
+    `const mod = require('./${cjsName}.js');`,
+    '',
+    `export const { ${names.join(', ')} } = mod;`,
+    'export default mod;',
+    ''
+  ].join('\n');
+  fs.writeFileSync(path.join(distDir, `${cjsName}.mjs`), body);
+  console.error(`created dist/${cjsName}.mjs`);
 }
+
+copy('node.js', 'node.js');
+copy('index.js', 'index.js');
+copy('web.js', 'web.mjs');
+esmWrapper('node');
+esmWrapper('index');
diff --git a/npm/lean-agentic/scripts/check-package.mjs b/npm/lean-agentic/scripts/check-package.mjs
new file mode 100644
index 0000000..63a3095
--- /dev/null
+++ b/npm/lean-agentic/scripts/check-package.mjs
@@ -0,0 +1,164 @@
+#!/usr/bin/env node
+/**
+ * Install lean-agentic into a fresh temp project and check what a user gets:
+ * every documented entry point loads under require and import, the CLI runs,
+ * and the MCP server's stdout carries nothing but JSON-RPC.
+ *
+ * Usage:
+ *   node scripts/check-package.mjs ./lean-agentic-0.3.4.tgz   # packed tarball
+ *   node scripts/check-package.mjs lean-agentic@0.3.4         # from the registry
+ */
+
+import { execFileSync, spawn, spawnSync } from 'node:child_process';
+import { existsSync, mkdtempSync, rmSync, writeFileSync } from 'node:fs';
+import { tmpdir } from 'node:os';
+import { join, resolve } from 'node:path';
+
+const spec = process.argv[2];
+if (!spec) {
+  console.error('usage: check-package.mjs <tarball | package spec>');
+  process.exit(2);
+}
+const installSpec = existsSync(spec) ? resolve(spec) : spec;
+
+const dir = mkdtempSync(join(tmpdir(), 'lean-agentic-check-'));
+let failures = 0;
+
+function pass(name) {
+  console.log(`ok   ${name}`);
+}
+
+function fail(name, detail) {
+  failures++;
+  console.log(`FAIL ${name}`);
+  if (detail) console.log(String(detail).trim().replace(/^/gm, '     '));
+}
+
+function runNode(args, input) {
+  return spawnSync(process.execPath, args, {
+    cwd: dir,
+    input,
+    encoding: 'utf8',
+    timeout: 60_000
+  });
+}
+
+try {
+  writeFileSync(join(dir, 'package.json'), JSON.stringify({ name: 'check', version: '1.0.0', private: true }));
+  execFileSync('npm', ['install', '--no-audit', '--no-fund', '--loglevel=error', installSpec], {
+    cwd: dir,
+    stdio: ['ignore', 'ignore', 'inherit'],
+    timeout: 300_000
+  });
+  pass(`install ${spec}`);
+
+  // Each case runs in its own process. It must print exactly the marker line
+  // on stdout: anything else (e.g. WASM init logs) is a failure.
+  const useDemo = `
+    const d = m.createDemo();
+    for (const k of ['createIdentity', 'createApplication', 'demonstrateHashConsing', 'getStats']) JSON.parse(d[k]());
+  `;
+  const cases = [
+    ['require("lean-agentic")', ['-e', `const m = require('lean-agentic'); ${useDemo} if (typeof m.init !== 'function') throw new Error('init missing'); console.log('MARK')`]],
+    ['import "lean-agentic"', ['--input-type=module', '-e', `import * as m from 'lean-agentic'; import def from 'lean-agentic'; ${useDemo} await m.init(); if (def.createDemo !== m.createDemo) throw new Error('default export mismatch'); console.log('MARK')`]],
+    ['require("lean-agentic/node")', ['-e', `const m = require('lean-agentic/node'); ${useDemo} console.log('MARK')`]],
+    ['import "lean-agentic/node"', ['--input-type=module', '-e', `import * as m from 'lean-agentic/node'; ${useDemo} console.log('MARK')`]],
+    ['import "lean-agentic/web"', ['--input-type=module', '-e', `import * as m from 'lean-agentic/web'; for (const k of ['initWeb', 'createDemo', 'setDebug']) if (typeof m[k] !== 'function') throw new Error(k + ' missing'); console.log('MARK')`]],
+    ['require("lean-agentic/package.json")', ['-e', `const p = require('lean-agentic/package.json'); if (!p.version) throw new Error('no version'); console.log('MARK')`]],
+    ['LEAN_AGENTIC_DEBUG logs to stderr only', ['-e', `process.env.LEAN_AGENTIC_DEBUG = '1'; const m = require('lean-agentic/node'); m.createDemo().createIdentity(); console.log('MARK')`]]
+  ];
+  for (const [name, args] of cases) {
+    const r = runNode(args);
+    if (r.status === 0 && r.stdout === 'MARK\n') pass(name);
+    else fail(name, `exit ${r.status}\nstdout: ${JSON.stringify(r.stdout)}\nstderr: ${r.stderr}`);
+  }
+
+  // CLI
+  const bin = join(dir, 'node_modules', 'lean-agentic', 'cli', 'index.js');
+  for (const args of [['--version'], ['demo']]) {
+    const r = runNode([bin, ...args]);
+    if (r.status === 0 && r.stdout.trim()) pass(`cli ${args.join(' ')}`);
+    else fail(`cli ${args.join(' ')}`, `exit ${r.status}\n${r.stdout}\n${r.stderr}`);
+  }
+
+  // MCP over stdio: initialize, the initialized notification, then tool calls
+  // that construct the WASM demo (where the old logs came from).
+  const requests = [
+    { jsonrpc: '2.0', id: 1, method: 'initialize', params: { protocolVersion: '2024-11-05', capabilities: {}, clientInfo: { name: 'check', version: '1' } } },
+    { jsonrpc: '2.0', method: 'notifications/initialized' },
+    { jsonrpc: '2.0', id: 2, method: 'tools/call', params: { name: 'create_identity', arguments: {} } },
+    { jsonrpc: '2.0', id: 3, method: 'tools/call', params: { name: 'demonstrate_hash_consing', arguments: {} } }
+  ];
+  const input = requests.map((r) => JSON.stringify(r)).join('\n') + '\n';
+  const servers = [
+    ['mcp/server.js', [join(dir, 'node_modules', 'lean-agentic', 'mcp', 'server.js')]],
+    ['cli mcp start', [bin, 'mcp', 'start']]
+  ];
+  for (const [name, args] of servers) {
+    const out = await runServer(args, input, 3);
+    const lines = out.split('\n').filter((l) => l.length > 0);
+    const problems = [];
+    let first;
+    try {
+      first = JSON.parse(lines[0]);
+    } catch {
+      problems.push(`first stdout line is not JSON: ${JSON.stringify(lines[0])}`);
+    }
+    if (first && !(first.jsonrpc === '2.0' && first.id === 1 && first.result)) {
+      problems.push(`first stdout line is not the initialize result: ${lines[0]}`);
+    }
+    const ids = [];
+    for (const line of lines) {
+      try {
+        const msg = JSON.parse(line);
+        if (msg.jsonrpc !== '2.0') problems.push(`not JSON-RPC 2.0: ${line}`);
+        if (msg.error) problems.push(`error response: ${line}`);
+        ids.push(msg.id);
+      } catch {
+        problems.push(`non-JSON stdout line: ${JSON.stringify(line)}`);
+      }
+    }
+    if (ids.join(',') !== '1,2,3') problems.push(`expected responses to ids 1,2,3, got ${ids.join(',')}`);
+    if (problems.length === 0) pass(`MCP stdio (${name}): ${lines.length} JSON-RPC lines, nothing else`);
+    else fail(`MCP stdio (${name})`, problems.join('\n'));
+  }
+} catch (error) {
+  fail('setup', error.stack || error);
+} finally {
+  rmSync(dir, { recursive: true, force: true });
+}
+
+if (failures) {
+  console.log(`\n${failures} check(s) failed`);
+  process.exit(1);
+}
+console.log('\nall checks passed');
+
+/**
+ * Start the server, write the requests, wait for `expected` responses (or 30s),
+ * then close stdin and kill the process. Resolves with everything on stdout.
+ */
+function runServer(args, input, expected) {
+  return new Promise((resolvePromise) => {
+    const child = spawn(process.execPath, args, { cwd: dir, stdio: ['pipe', 'pipe', 'ignore'] });
+    let out = '';
+    const finish = () => {
+      clearTimeout(timer);
+      child.stdin.end();
+      setTimeout(() => {
+        child.kill();
+        resolvePromise(out);
+      }, 200);
+    };
+    const timer = setTimeout(finish, 30_000);
+    child.stdout.on('data', (chunk) => {
+      out += chunk;
+      if (out.split('\n').filter(Boolean).length >= expected) finish();
+    });
+    child.on('exit', () => {
+      clearTimeout(timer);
+      resolvePromise(out);
+    });
+    child.stdin.write(input);
+  });
+}
diff --git a/npm/lean-agentic/src/index.js b/npm/lean-agentic/src/index.js
index 9eec57c..c94e0b2 100644
--- a/npm/lean-agentic/src/index.js
+++ b/npm/lean-agentic/src/index.js
@@ -1,81 +1,29 @@
 /**
  * lean-agentic - Hash-consed dependent types with 150x faster equality
  *
+ * Root entry point. Under Node.js this is the same API as `lean-agentic/node`,
+ * plus an `init()` that resolves immediately (the Node WASM build loads
+ * synchronously). Browsers should use `lean-agentic/web`.
+ *
  * @module lean-agentic
  * @author ruv.io
  * @license Apache-2.0
  */
 
-import * as wasm from '../wasm/leanr_wasm.js';
+const node = require('./node.js');
 
 /**
- * Initialize the WASM module
+ * Kept for API compatibility: the Node WASM build is ready as soon as it is
+ * required, so there is nothing to wait for.
  * @returns {Promise<void>}
  */
-export async function init() {
-  // WASM is already initialized when imported
-  return Promise.resolve();
-}
-
-/**
- * LeanDemo - Main interface for lean-agentic
- */
-export class LeanDemo {
-  constructor() {
-    this._inner = new wasm.LeanDemo();
-  }
-
-  /**
-   * Create identity function: λx:Type. x
-   * @returns {string} JSON representation of the identity function
-   */
-  createIdentity() {
-    return this._inner.create_identity();
-  }
-
-  /**
-   * Create and verify an application
-   * @returns {string} JSON representation of the application
-   */
-  createApplication() {
-    return this._inner.create_application();
-  }
-
-  /**
-   * Demonstrate hash-consing by creating identical terms
-   * @returns {string} JSON showing term equality
-   */
-  demonstrateHashConsing() {
-    return this._inner.demonstrate_hash_consing();
-  }
-}
-
-/**
- * Create a new LeanDemo instance
- * @returns {LeanDemo}
- */
-export function createDemo() {
-  return new LeanDemo();
-}
-
-/**
- * Quick start: Create identity function
- * @returns {Promise<string>}
- */
-export async function quickStart() {
-  await init();
-  const demo = createDemo();
-  return demo.createIdentity();
-}
-
-// Re-export WASM types
-export { wasm };
+async function init() {}
 
-// Default export
-export default {
+module.exports = {
   init,
-  LeanDemo,
-  createDemo,
-  quickStart,
-  wasm
+  LeanDemo: node.LeanDemo,
+  createDemo: node.createDemo,
+  quickStart: node.quickStart,
+  setDebug: node.setDebug,
+  wasm: node.wasm
 };
diff --git a/npm/lean-agentic/src/node.js b/npm/lean-agentic/src/node.js
index 535c5b7..3c03817 100644
--- a/npm/lean-agentic/src/node.js
+++ b/npm/lean-agentic/src/node.js
@@ -8,6 +8,19 @@
 
 const wasm = require('../wasm-node/leanr_wasm.js');
 
+/**
+ * Turn the WASM module's diagnostic logging on or off. Logs go to stderr
+ * (console.error), never stdout. Off by default; set LEAN_AGENTIC_DEBUG=1
+ * to turn it on at load time.
+ * @param {boolean} enabled
+ */
+function setDebug(enabled) {
+  wasm.setDebug(Boolean(enabled));
+}
+
+const debugEnv = process.env.LEAN_AGENTIC_DEBUG;
+setDebug(debugEnv !== undefined && debugEnv !== '' && debugEnv !== '0' && debugEnv !== 'false');
+
 /**
  * LeanDemo - Node.js interface
  */
@@ -78,5 +91,6 @@ module.exports = {
   LeanDemo,
   createDemo,
   quickStart,
+  setDebug,
   wasm
 };
diff --git a/npm/lean-agentic/src/web.js b/npm/lean-agentic/src/web.js
index 05aa215..5920b7c 100644
--- a/npm/lean-agentic/src/web.js
+++ b/npm/lean-agentic/src/web.js
@@ -87,6 +87,15 @@ export class LeanDemo {
   }
 }
 
+/**
+ * Turn the WASM module's diagnostic logging (console.error) on or off.
+ * Off by default. Call after initWeb().
+ * @param {boolean} enabled
+ */
+export function setDebug(enabled) {
+  wasm.setDebug(Boolean(enabled));
+}
+
 export function createDemo() {
   return new LeanDemo();
 }
@@ -95,5 +104,6 @@ export default {
   initWeb,
   LeanDemo,
   createDemo,
+  setDebug,
   wasm
 };
diff --git a/npm/lean-agentic/wasm-node/leanr_wasm.d.ts b/npm/lean-agentic/wasm-node/leanr_wasm.d.ts
index ae5435f..54f6f8b 100644
--- a/npm/lean-agentic/wasm-node/leanr_wasm.d.ts
+++ b/npm/lean-agentic/wasm-node/leanr_wasm.d.ts
@@ -1,5 +1,9 @@
 /* tslint:disable */
 /* eslint-disable */
+/**
+ * Turn diagnostic logging on or off (off by default).
+ */
+export function setDebug(enabled: boolean): void;
 /**
  * Simple greeting function for testing WASM works
  */
@@ -15,33 +19,33 @@ export class LeanDemo {
   free(): void;
   [Symbol.dispose](): void;
   /**
-   * Create a new Lean demo instance
+   * Create a simple type (Type universe)
    */
-  constructor();
+  createType(): boolean;
   /**
    * Demonstrate hash-consing: creating same term twice reuses memory
    * Returns true if successful
    */
   createVariable(index: number): boolean;
   /**
-   * Create two identical variables and verify they share the same ID
-   * Returns true if hash-consing worked (same IDs)
+   * Verify that hash-consing provides O(1) equality
    */
-  demonstrateHashConsing(): boolean;
+  benchmarkEquality(): string;
   /**
-   * Get statistics about the arena (number of unique terms)
+   * Create a lambda abstraction (x : Type) => x
    */
-  getStats(): string;
+  createIdentityFunction(): boolean;
   /**
-   * Create a simple type (Type universe)
+   * Create two identical variables and verify they share the same ID
+   * Returns true if hash-consing worked (same IDs)
    */
-  createType(): boolean;
+  demonstrateHashConsing(): boolean;
   /**
-   * Create a lambda abstraction (x : Type) => x
+   * Create a new Lean demo instance
    */
-  createIdentityFunction(): boolean;
+  constructor();
   /**
-   * Verify that hash-consing provides O(1) equality
+   * Get statistics about the arena (number of unique terms)
    */
-  benchmarkEquality(): string;
+  getStats(): string;
 }
diff --git a/npm/lean-agentic/wasm-node/leanr_wasm.js b/npm/lean-agentic/wasm-node/leanr_wasm.js
index 4182fef..a2a3a6b 100644
--- a/npm/lean-agentic/wasm-node/leanr_wasm.js
+++ b/npm/lean-agentic/wasm-node/leanr_wasm.js
@@ -23,6 +23,13 @@ function getStringFromWasm0(ptr, len) {
     ptr = ptr >>> 0;
     return decodeText(ptr, len);
 }
+/**
+ * Turn diagnostic logging on or off (off by default).
+ * @param {boolean} enabled
+ */
+exports.setDebug = function(enabled) {
+    wasm.setDebug(enabled);
+};
 
 let WASM_VECTOR_LEN = 0;
 
@@ -134,13 +141,12 @@ class LeanDemo {
         wasm.__wbg_leandemo_free(ptr, 0);
     }
     /**
-     * Create a new Lean demo instance
+     * Create a simple type (Type universe)
+     * @returns {boolean}
      */
-    constructor() {
-        const ret = wasm.leandemo_new();
-        this.__wbg_ptr = ret >>> 0;
-        LeanDemoFinalization.register(this, this.__wbg_ptr, this);
-        return this;
+    createType() {
+        const ret = wasm.leandemo_createType(this.__wbg_ptr);
+        return ret !== 0;
     }
     /**
      * Demonstrate hash-consing: creating same term twice reuses memory
@@ -153,23 +159,14 @@ class LeanDemo {
         return ret !== 0;
     }
     /**
-     * Create two identical variables and verify they share the same ID
-     * Returns true if hash-consing worked (same IDs)
-     * @returns {boolean}
-     */
-    demonstrateHashConsing() {
-        const ret = wasm.leandemo_demonstrateHashConsing(this.__wbg_ptr);
-        return ret !== 0;
-    }
-    /**
-     * Get statistics about the arena (number of unique terms)
+     * Verify that hash-consing provides O(1) equality
      * @returns {string}
      */
-    getStats() {
+    benchmarkEquality() {
         let deferred1_0;
         let deferred1_1;
         try {
-            const ret = wasm.leandemo_getStats(this.__wbg_ptr);
+            const ret = wasm.leandemo_benchmarkEquality(this.__wbg_ptr);
             deferred1_0 = ret[0];
             deferred1_1 = ret[1];
             return getStringFromWasm0(ret[0], ret[1]);
@@ -178,30 +175,40 @@ class LeanDemo {
         }
     }
     /**
-     * Create a simple type (Type universe)
+     * Create a lambda abstraction (x : Type) => x
      * @returns {boolean}
      */
-    createType() {
-        const ret = wasm.leandemo_createType(this.__wbg_ptr);
+    createIdentityFunction() {
+        const ret = wasm.leandemo_createIdentityFunction(this.__wbg_ptr);
         return ret !== 0;
     }
     /**
-     * Create a lambda abstraction (x : Type) => x
+     * Create two identical variables and verify they share the same ID
+     * Returns true if hash-consing worked (same IDs)
      * @returns {boolean}
      */
-    createIdentityFunction() {
-        const ret = wasm.leandemo_createIdentityFunction(this.__wbg_ptr);
+    demonstrateHashConsing() {
+        const ret = wasm.leandemo_demonstrateHashConsing(this.__wbg_ptr);
         return ret !== 0;
     }
     /**
-     * Verify that hash-consing provides O(1) equality
+     * Create a new Lean demo instance
+     */
+    constructor() {
+        const ret = wasm.leandemo_new();
+        this.__wbg_ptr = ret >>> 0;
+        LeanDemoFinalization.register(this, this.__wbg_ptr, this);
+        return this;
+    }
+    /**
+     * Get statistics about the arena (number of unique terms)
      * @returns {string}
      */
-    benchmarkEquality() {
+    getStats() {
         let deferred1_0;
         let deferred1_1;
         try {
-            const ret = wasm.leandemo_benchmarkEquality(this.__wbg_ptr);
+            const ret = wasm.leandemo_getStats(this.__wbg_ptr);
             deferred1_0 = ret[0];
             deferred1_1 = ret[1];
             return getStringFromWasm0(ret[0], ret[1]);
@@ -214,8 +221,8 @@ if (Symbol.dispose) LeanDemo.prototype[Symbol.dispose] = LeanDemo.prototype.free
 
 exports.LeanDemo = LeanDemo;
 
-exports.__wbg_log_6c7b5f4f00b8ce3f = function(arg0) {
-    console.log(arg0);
+exports.__wbg_error_99981e16d476aa5c = function(arg0) {
+    console.error(arg0);
 };
 
 exports.__wbg_wbindgenthrow_451ec1a8469d7eb6 = function(arg0, arg1) {
diff --git a/npm/lean-agentic/wasm-node/leanr_wasm_bg.wasm b/npm/lean-agentic/wasm-node/leanr_wasm_bg.wasm
index a69fdf4..993444e 100644
Binary files a/npm/lean-agentic/wasm-node/leanr_wasm_bg.wasm and b/npm/lean-agentic/wasm-node/leanr_wasm_bg.wasm differ
diff --git a/npm/lean-agentic/wasm-node/leanr_wasm_bg.wasm.d.ts b/npm/lean-agentic/wasm-node/leanr_wasm_bg.wasm.d.ts
index 0b0167a..33b0566 100644
--- a/npm/lean-agentic/wasm-node/leanr_wasm_bg.wasm.d.ts
+++ b/npm/lean-agentic/wasm-node/leanr_wasm_bg.wasm.d.ts
@@ -2,17 +2,18 @@
 /* eslint-disable */
 export const memory: WebAssembly.Memory;
 export const __wbg_leandemo_free: (a: number, b: number) => void;
-export const leandemo_new: () => number;
+export const getVersion: () => [number, number];
+export const greet: (a: number, b: number) => [number, number];
+export const leandemo_benchmarkEquality: (a: number) => [number, number];
+export const leandemo_createIdentityFunction: (a: number) => number;
+export const leandemo_createType: (a: number) => number;
 export const leandemo_createVariable: (a: number, b: number) => number;
 export const leandemo_demonstrateHashConsing: (a: number) => number;
 export const leandemo_getStats: (a: number) => [number, number];
-export const leandemo_createType: (a: number) => number;
-export const leandemo_createIdentityFunction: (a: number) => number;
-export const leandemo_benchmarkEquality: (a: number) => [number, number];
-export const greet: (a: number, b: number) => [number, number];
-export const getVersion: () => [number, number];
+export const leandemo_new: () => number;
+export const setDebug: (a: number) => void;
 export const __wbindgen_export_0: WebAssembly.Table;
-export const __wbindgen_free: (a: number, b: number, c: number) => void;
 export const __wbindgen_malloc: (a: number, b: number) => number;
 export const __wbindgen_realloc: (a: number, b: number, c: number, d: number) => number;
+export const __wbindgen_free: (a: number, b: number, c: number) => void;
 export const __wbindgen_start: () => void;
diff --git a/npm/lean-agentic/wasm-node/package.json b/npm/lean-agentic/wasm-node/package.json
index 6b74ad0..d93d6c0 100644
--- a/npm/lean-agentic/wasm-node/package.json
+++ b/npm/lean-agentic/wasm-node/package.json
@@ -5,7 +5,7 @@
     "github.com/ruvnet"
   ],
   "description": "WebAssembly bindings for lean-agentic: hash-consed dependent types in the browser",
-  "version": "0.1.0",
+  "version": "0.3.0",
   "license": "Apache-2.0",
   "repository": {
     "type": "git",
diff --git a/npm/lean-agentic/wasm-web/leanr_wasm.d.ts b/npm/lean-agentic/wasm-web/leanr_wasm.d.ts
index 23a87dc..dbfe76d 100644
--- a/npm/lean-agentic/wasm-web/leanr_wasm.d.ts
+++ b/npm/lean-agentic/wasm-web/leanr_wasm.d.ts
@@ -1,5 +1,9 @@
 /* tslint:disable */
 /* eslint-disable */
+/**
+ * Turn diagnostic logging on or off (off by default).
+ */
+export function setDebug(enabled: boolean): void;
 /**
  * Simple greeting function for testing WASM works
  */
@@ -15,35 +19,35 @@ export class LeanDemo {
   free(): void;
   [Symbol.dispose](): void;
   /**
-   * Create a new Lean demo instance
+   * Create a simple type (Type universe)
    */
-  constructor();
+  createType(): boolean;
   /**
    * Demonstrate hash-consing: creating same term twice reuses memory
    * Returns true if successful
    */
   createVariable(index: number): boolean;
   /**
-   * Create two identical variables and verify they share the same ID
-   * Returns true if hash-consing worked (same IDs)
+   * Verify that hash-consing provides O(1) equality
    */
-  demonstrateHashConsing(): boolean;
+  benchmarkEquality(): string;
   /**
-   * Get statistics about the arena (number of unique terms)
+   * Create a lambda abstraction (x : Type) => x
    */
-  getStats(): string;
+  createIdentityFunction(): boolean;
   /**
-   * Create a simple type (Type universe)
+   * Create two identical variables and verify they share the same ID
+   * Returns true if hash-consing worked (same IDs)
    */
-  createType(): boolean;
+  demonstrateHashConsing(): boolean;
   /**
-   * Create a lambda abstraction (x : Type) => x
+   * Create a new Lean demo instance
    */
-  createIdentityFunction(): boolean;
+  constructor();
   /**
-   * Verify that hash-consing provides O(1) equality
+   * Get statistics about the arena (number of unique terms)
    */
-  benchmarkEquality(): string;
+  getStats(): string;
 }
 
 export type InitInput = RequestInfo | URL | Response | BufferSource | WebAssembly.Module;
@@ -51,19 +55,20 @@ export type InitInput = RequestInfo | URL | Response | BufferSource | WebAssembl
 export interface InitOutput {
   readonly memory: WebAssembly.Memory;
   readonly __wbg_leandemo_free: (a: number, b: number) => void;
-  readonly leandemo_new: () => number;
+  readonly getVersion: () => [number, number];
+  readonly greet: (a: number, b: number) => [number, number];
+  readonly leandemo_benchmarkEquality: (a: number) => [number, number];
+  readonly leandemo_createIdentityFunction: (a: number) => number;
+  readonly leandemo_createType: (a: number) => number;
   readonly leandemo_createVariable: (a: number, b: number) => number;
   readonly leandemo_demonstrateHashConsing: (a: number) => number;
   readonly leandemo_getStats: (a: number) => [number, number];
-  readonly leandemo_createType: (a: number) => number;
-  readonly leandemo_createIdentityFunction: (a: number) => number;
-  readonly leandemo_benchmarkEquality: (a: number) => [number, number];
-  readonly greet: (a: number, b: number) => [number, number];
-  readonly getVersion: () => [number, number];
+  readonly leandemo_new: () => number;
+  readonly setDebug: (a: number) => void;
   readonly __wbindgen_export_0: WebAssembly.Table;
-  readonly __wbindgen_free: (a: number, b: number, c: number) => void;
   readonly __wbindgen_malloc: (a: number, b: number) => number;
   readonly __wbindgen_realloc: (a: number, b: number, c: number, d: number) => number;
+  readonly __wbindgen_free: (a: number, b: number, c: number) => void;
   readonly __wbindgen_start: () => void;
 }
 
diff --git a/npm/lean-agentic/wasm-web/leanr_wasm.js b/npm/lean-agentic/wasm-web/leanr_wasm.js
index 5fdddc2..8b9531f 100644
--- a/npm/lean-agentic/wasm-web/leanr_wasm.js
+++ b/npm/lean-agentic/wasm-web/leanr_wasm.js
@@ -29,6 +29,13 @@ function getStringFromWasm0(ptr, len) {
     ptr = ptr >>> 0;
     return decodeText(ptr, len);
 }
+/**
+ * Turn diagnostic logging on or off (off by default).
+ * @param {boolean} enabled
+ */
+export function setDebug(enabled) {
+    wasm.setDebug(enabled);
+}
 
 let WASM_VECTOR_LEN = 0;
 
@@ -140,13 +147,12 @@ export class LeanDemo {
         wasm.__wbg_leandemo_free(ptr, 0);
     }
     /**
-     * Create a new Lean demo instance
+     * Create a simple type (Type universe)
+     * @returns {boolean}
      */
-    constructor() {
-        const ret = wasm.leandemo_new();
-        this.__wbg_ptr = ret >>> 0;
-        LeanDemoFinalization.register(this, this.__wbg_ptr, this);
-        return this;
+    createType() {
+        const ret = wasm.leandemo_createType(this.__wbg_ptr);
+        return ret !== 0;
     }
     /**
      * Demonstrate hash-consing: creating same term twice reuses memory
@@ -159,23 +165,14 @@ export class LeanDemo {
         return ret !== 0;
     }
     /**
-     * Create two identical variables and verify they share the same ID
-     * Returns true if hash-consing worked (same IDs)
-     * @returns {boolean}
-     */
-    demonstrateHashConsing() {
-        const ret = wasm.leandemo_demonstrateHashConsing(this.__wbg_ptr);
-        return ret !== 0;
-    }
-    /**
-     * Get statistics about the arena (number of unique terms)
+     * Verify that hash-consing provides O(1) equality
      * @returns {string}
      */
-    getStats() {
+    benchmarkEquality() {
         let deferred1_0;
         let deferred1_1;
         try {
-            const ret = wasm.leandemo_getStats(this.__wbg_ptr);
+            const ret = wasm.leandemo_benchmarkEquality(this.__wbg_ptr);
             deferred1_0 = ret[0];
             deferred1_1 = ret[1];
             return getStringFromWasm0(ret[0], ret[1]);
@@ -184,30 +181,40 @@ export class LeanDemo {
         }
     }
     /**
-     * Create a simple type (Type universe)
+     * Create a lambda abstraction (x : Type) => x
      * @returns {boolean}
      */
-    createType() {
-        const ret = wasm.leandemo_createType(this.__wbg_ptr);
+    createIdentityFunction() {
+        const ret = wasm.leandemo_createIdentityFunction(this.__wbg_ptr);
         return ret !== 0;
     }
     /**
-     * Create a lambda abstraction (x : Type) => x
+     * Create two identical variables and verify they share the same ID
+     * Returns true if hash-consing worked (same IDs)
      * @returns {boolean}
      */
-    createIdentityFunction() {
-        const ret = wasm.leandemo_createIdentityFunction(this.__wbg_ptr);
+    demonstrateHashConsing() {
+        const ret = wasm.leandemo_demonstrateHashConsing(this.__wbg_ptr);
         return ret !== 0;
     }
     /**
-     * Verify that hash-consing provides O(1) equality
+     * Create a new Lean demo instance
+     */
+    constructor() {
+        const ret = wasm.leandemo_new();
+        this.__wbg_ptr = ret >>> 0;
+        LeanDemoFinalization.register(this, this.__wbg_ptr, this);
+        return this;
+    }
+    /**
+     * Get statistics about the arena (number of unique terms)
      * @returns {string}
      */
-    benchmarkEquality() {
+    getStats() {
         let deferred1_0;
         let deferred1_1;
         try {
-            const ret = wasm.leandemo_benchmarkEquality(this.__wbg_ptr);
+            const ret = wasm.leandemo_getStats(this.__wbg_ptr);
             deferred1_0 = ret[0];
             deferred1_1 = ret[1];
             return getStringFromWasm0(ret[0], ret[1]);
@@ -256,8 +263,8 @@ async function __wbg_load(module, imports) {
 function __wbg_get_imports() {
     const imports = {};
     imports.wbg = {};
-    imports.wbg.__wbg_log_6c7b5f4f00b8ce3f = function(arg0) {
-        console.log(arg0);
+    imports.wbg.__wbg_error_99981e16d476aa5c = function(arg0) {
+        console.error(arg0);
     };
     imports.wbg.__wbg_wbindgenthrow_451ec1a8469d7eb6 = function(arg0, arg1) {
         throw new Error(getStringFromWasm0(arg0, arg1));
diff --git a/npm/lean-agentic/wasm-web/leanr_wasm_bg.wasm b/npm/lean-agentic/wasm-web/leanr_wasm_bg.wasm
index 6ff95d5..e32254b 100644
Binary files a/npm/lean-agentic/wasm-web/leanr_wasm_bg.wasm and b/npm/lean-agentic/wasm-web/leanr_wasm_bg.wasm differ
diff --git a/npm/lean-agentic/wasm-web/leanr_wasm_bg.wasm.d.ts b/npm/lean-agentic/wasm-web/leanr_wasm_bg.wasm.d.ts
index 0b0167a..33b0566 100644
--- a/npm/lean-agentic/wasm-web/leanr_wasm_bg.wasm.d.ts
+++ b/npm/lean-agentic/wasm-web/leanr_wasm_bg.wasm.d.ts
@@ -2,17 +2,18 @@
 /* eslint-disable */
 export const memory: WebAssembly.Memory;
 export const __wbg_leandemo_free: (a: number, b: number) => void;
-export const leandemo_new: () => number;
+export const getVersion: () => [number, number];
+export const greet: (a: number, b: number) => [number, number];
+export const leandemo_benchmarkEquality: (a: number) => [number, number];
+export const leandemo_createIdentityFunction: (a: number) => number;
+export const leandemo_createType: (a: number) => number;
 export const leandemo_createVariable: (a: number, b: number) => number;
 export const leandemo_demonstrateHashConsing: (a: number) => number;
 export const leandemo_getStats: (a: number) => [number, number];
-export const leandemo_createType: (a: number) => number;
-export const leandemo_createIdentityFunction: (a: number) => number;
-export const leandemo_benchmarkEquality: (a: number) => [number, number];
-export const greet: (a: number, b: number) => [number, number];
-export const getVersion: () => [number, number];
+export const leandemo_new: () => number;
+export const setDebug: (a: number) => void;
 export const __wbindgen_export_0: WebAssembly.Table;
-export const __wbindgen_free: (a: number, b: number, c: number) => void;
 export const __wbindgen_malloc: (a: number, b: number) => number;
 export const __wbindgen_realloc: (a: number, b: number, c: number, d: number) => number;
+export const __wbindgen_free: (a: number, b: number, c: number) => void;
 export const __wbindgen_start: () => void;
diff --git a/npm/lean-agentic/wasm-web/package.json b/npm/lean-agentic/wasm-web/package.json
index a1478c6..a415055 100644
--- a/npm/lean-agentic/wasm-web/package.json
+++ b/npm/lean-agentic/wasm-web/package.json
@@ -6,7 +6,7 @@
     "github.com/ruvnet"
   ],
   "description": "WebAssembly bindings for lean-agentic: hash-consed dependent types in the browser",
-  "version": "0.1.0",
+  "version": "0.3.0",
   "license": "Apache-2.0",
   "repository": {
     "type": "git",