Skip to main content
The Z3 JavaScript/TypeScript bindings are distributed as the z3-solver package on npm. Z3 is compiled to WebAssembly and included as part of the package, so no separate Z3 installation is required.

​
Requirements

  • Node.js 16 or later
  • npm or yarn package manager
  • Modern browser with SharedArrayBuffer support
  • Special COOP/COEP headers required (see below)
  • Chrome 92+, Firefox 89+, Safari 15.2+, or Edge 92+

​
Installation

npm install z3-solver

​
Package Information

The z3-solver package includes:
  • WebAssembly artifact: Pre-compiled Z3 as a WASM module
  • TypeScript bindings: High-level and low-level APIs
  • Type definitions: Full TypeScript types for IDE support
  • Browser and Node.js support: Automatic platform detection

​
Package Details

​
version
string
Current version: 0.1.0
​
keywords
array
Z3, theorem, prover, solver, satisfiability, smt
​
engines
object
Node.js >= 16 required

​
Browser Setup

Browser usage requires SharedArrayBuffer, which needs special HTTP headers for security.

​
Required Headers

Your web server must send these headers: 
Cross-Origin-Opener-Policy: same-origin
Cross-Origin-Embedder-Policy: require-corp

​
Development Setup

For local development or static hosting (e.g., GitHub Pages), you can use the coi-serviceworker trick:
index.html
<!DOCTYPE html>
<html>
<head>
  <!-- Load COI service worker for local development -->
  <script src="https://unpkg.com/[email protected]/coi-serviceworker.min.js"></script>
</head>
<body>
  <script type="module" src="./main.js"></script>
</body>
</html>
The COI service worker trick is great for development and demos, but not recommended for production applications with complex service worker requirements.

​
Production Setup

For production, configure your web server properly: 
add_header Cross-Origin-Opener-Policy same-origin;
add_header Cross-Origin-Embedder-Policy require-corp;

​
Manual Import

The package auto-detects your environment, but you can import explicitly: 
const { init } = require('z3-solver/node');

​
Bundler Configuration

​
Webpack

When using webpack, ensure z3-built.js is included as a separate script:
webpack.config.js
module.exports = {
  // ... other config
  output: {
    filename: '[name].bundle.js',
    path: path.resolve(__dirname, 'dist'),
  },
  plugins: [
    new CopyWebpackPlugin({
      patterns: [
        {
          from: 'node_modules/z3-solver/build/z3-built.js',
          to: 'z3-built.js'
        }
      ]
    })
  ]
};

​
Vite

Vite should work out of the box with proper headers configured.

​
Verification

Verify your installation:
test.js
const { init } = require('z3-solver');

(async () => {
  const { Context } = await init();
  const { Int, Solver } = new Context('main');
  
  const x = Int.const('x');
  const solver = new Solver();
  solver.add(x.gt(0));
  
  const result = await solver.check();
  console.log('Installation successful! Result:', result);
})();
Run it: 
node test.js
Expected output: 
Installation successful! Result: sat

​
Troubleshooting

Browser: Ensure COOP/COEP headers are set correctly. Check browser console for specific error messages.Node.js: Update to Node.js 16 or later.
When using bundlers like webpack, ensure z3-built.js is included as a separate script file, not bundled into your main application bundle.
Clear your node_modules and reinstall:
rm -rf node_modules package-lock.json
npm install
Ensure your tsconfig.json includes:
{
  "compilerOptions": {
    "moduleResolution": "node",
    "esModuleInterop": true,
    "lib": ["ES2020", "DOM"]
  }
}

​
Next Steps

Getting Started

Learn the basics with quick examples

API Reference

Explore the complete API

Build docs developers (and LLMs) love

Get started for freeTalk to us