Program Verification for ECMAScript/JavaScript (esverify.org).

Alpha: This is still a research prototype and not yet ready for production use.

Documentation

A detailed documentation of esverify and its theoretical foundations is currently work-in-progress and will be published soon.

Example

Given a simple JavaScript max function, we can add pre- and post-conditions using special pseudo-calls to requires and ensures with boolean expressions.

function max(a, b) {
  requires(typeof(a) === "number");
  requires(typeof(b) === "number");
  ensures(res => res >= a);

  if (a >= b) {
    return a;
  } else {
    return b;
  }
}

These expressions will then be statically verified with respect to the function body with an SMT solver.

More examples can be found in the tests directory.

Supported Features

It is based on the z3 SMT solver but avoids trigger heuristics and thereby timeouts and other unpredictable results by requiring manual instantiation with function calls which will be used for a deterministic trigger instantiation.

To Do

Usage as Command Line Tool

$ npm install -g esverify

...

$ esverify --help
Usage: esverify [OPTIONS] FILE

Options:
  -f, --logformat FORMAT  Format can be either "simple" or "colored"
                          (default format is "colored")
  --z3path PATH           Path to local z3 executable
                          (default path is "z3")
  -r, --remote            Invokes z3 remotely via HTTP request
  --z3url URL             URL to remote z3 web server
  -q, --quiet             Suppresses output
  -h, --help              Prints this help text and exit
  -v, --version           Prints version information

Usage as Library

Installation via npm:

$ npm install esverify --save

Can now import verify which returns a promise of messages:

import { verify } from "esverify";

const opts = { };
const msgs = await verify("assert(1 > 2);", opts);
msgs.forEach(msg => console.log(msg.status));

The options and returned messages have the following structure:

type opts = {
  filename: string,
  logformat: "simple" | "colored" = "colored",
  quiet: boolean = true,
  z3path: string = "z3",
  z3url: string,
  remote: boolean = false
}

type msg = {
  status: "verified" | "unverified" | "error",
  loc: { file: string, start: { line: number, column: number },
                       end:   { line: number, column: number }},
  description: string
}

Interactive Tools

More tool support will be coming soon.

A simple web-based editor is available online at esverify.org/try.

Additionally, there is a Vim Plugin which displays verification results inline.

Acknowledgements

Inspired by Dafny and LiquidHaskell.

This project is developed by the Software and Languages Research Group at University of California, Santa Cruz. Thanks also to Tommy, Sohum and Cormac for support and advice.