View the npm package here.

z3-solver works with JavaScript apps through bindings to WebAssembly.

Some important notes from the npm package:

With those notes in mind, let's get started integrating z3-solver into your Next.js app!

From your terminal, run npm install z3-solver.

Once installed, you'll need to copy some pre-built files that z3-solver provides into your application. If you're running z3-solver in a Node.js environment, i.e. using Server Actions in Next.js, you can skip this step. If you're using z3-solver client-side, i.e. in the browser, this is required.

Files:

• node_modules/z3-solver/build/z3-built.js
• node_modules/z3-solver/build/z3-built.wasm
• node_modules/z3-solver/build/z3-built.worker.js

You'll copy these files into your public directory in your Next.js app.

Add a <script> component to the page/component that requires the z3-solver package. You have two options here:

Option 1: Add a <script> component that loads the public file synchronously.

1
<script src="/z3-built.js" />

This will defer loading of your page/component until the script has been downloaded. This may hurt the first-time-to-load performance of your page, but is the easiest way to guarentee that the scripts have been loaded.

Be warned, Next.js will throw a @next/next/no-sync-scripts error when you try to build the app. You can disable this error, or you can try the option below.

Option 2: Add a <Script> component (from Next.js) that loads the public file asynchronously and updates state after loading.

1
2
3
4
<Script
    src="/z3-built.js"
    onLoad={() => setStatus("loaded")}
/>

Your page/component will be free to load in parallel, allowing a faster initial load of your page. You can then do fine-grain state management to prevent usage of the z3-solver package until the script has finished loading.

For z3-solver's JavaScript<->WASM bindings to work, the library requires that SharedArrayBuffer be availble in the browser. Every major browser supports SharedArrayBuffer, but only in a secure context.

To enable a secure context, you'll set two headers:

• "Cross-Origin-Opener-Policy" to "same-origin"
• "Cross-Origin-Embedder-Policy" to "require-corp"

Add the following to your Next.js config file (next.config.{js|ts|mjs}):

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
async headers() {
    return [
        {
            source: "/:path*", // Match all routes
            headers: [
                // These headers are required for z3-solver
                {
                    key: "Cross-Origin-Opener-Policy",
                    value: "same-origin",
                },
                {
                    key: "Cross-Origin-Embedder-Policy",
                    value: "require-corp",
                },
            ],
        },
    ];
},

1
2
3
4
5
6
7
8
9
10
11
12
13
// 1) Import
import { init } from "z3-solver";

...

// 2) Initialize
// You'll need to wait for your script to be loaded first
const { Context } = await init();

// 3) Create a Context
// Types fall over beyond here
// @ts-ignore
const { Solver, Int } = new Context("main");

After this, you should be set up to use z3-solver.

Because the documentation is a bit lacking and the TypeScript types don't work very well, it can be a bit challenging to know how you can use z3-solver in JavaScript.

To see what methods are available for the data types (Int, Real, BitVec, etc.), you can create one of those objects and console.log it. You'll see the Prototype methods for that object, which should give you an idea how you can use these objects.

The console.log output of a z3-solver Int object

If you'd like to see a real example of z3-solver being used, check out my Advent of Code 2024 Day 13 Part 2 solution.