z3js

0.0.0 verified Fri May 01 auth: no javascript

z3js is a tiny utility library (v0.0.0) for transpiling a small subset of JavaScript expressions to SMT2 format for use with the Z3 solver. It includes a JavaScript parser, a SMT2 code generator, and a minimal S-expression parser for reading Z3 outputs. The library is experimental and limited to simple variable declarations, function definitions, and assertions. It requires an external Z3 solver binary and is intended for prototyping program synthesis and formal verification tools. No releases or update cadence is established; the project appears to be in early development. Key differentiators: focuses on a tight JS→SMT2 bridge, unlike full verification frameworks.

Common errors

error Error: Cannot find module 'z3js' ↓

cause Package not installed or not installed correctly.

fix

Run npm install z3js or use a local path like 'require('./path/to/z3js/src')'.

error parse error: unexpected token ↓

cause JavaScript code contains unsupported syntax (e.g., arrow functions, let/const, templates).

fix

Rewrite using only 'var', function declarations, and simple expressions.

error z3: command not found ↓

cause Z3 solver binary is not installed or not in PATH.

fix

Install Z3 via 'brew install z3' (macOS) or 'sudo apt install z3' (Ubuntu) or download from GitHub.

Warnings

breaking The library is version 0.0.0 and API is unstable. No semVer guarantees. ↓

fix Pin to exact version and expect future breaking changes.

gotcha Requires external Z3 binary. Does not bundle or install Z3 automatically. ↓

fix Install Z3 via 'brew install z3' or 'apt install z3' and ensure it's in PATH.

gotcha Only a tiny subset of JavaScript is supported. For loops, arrays, objects, and closures are not supported. ↓

fix Refer to project examples for the supported syntax.

gotcha No TypeScript type definitions are provided. All types are lost when using this library. ↓

fix Use JSDoc or manually declare types if using TypeScript.

Install

npm install z3js

yarn add z3js

pnpm add z3js

Imports

jsParser

wrong

const jsParser = require('z3js').jsParser

correct

import { jsParser } from 'z3js'

No ESM module published; only CommonJS supported.

toSMT2
```
const { toSMT2 } = require('z3js')
```
Default export not available; always use named import.

declareDatatypes

wrong

import declareDatatypes from 'z3js'

correct

const { declareDatatypes } = require('z3js')

No default export; only named exports.

Quickstart

Transpile a small JS program with function and assertion to SMT2 and pipe to Z3 solver.

const { jsParser, toSMT2, declareDatatypes } = require('z3js');

const JS_CODE = `
var x;
function f(args) {
  return args.one * args.two;
}
assert(f(x) === 2);
check_sat();
get_model();
`;

const typeDefs = {
  x: '(Arg)',
  y: '(Arg)',
  f: {
    args: '(Arg)',
    return: 'Int'
  }
};

console.log(declareDatatypes('Arg', { one: 'Int', two: 'Int' }));
console.log(toSMT2(jsParser.parse(JS_CODE), typeDefs));