Cavalry

Cavalry is an imperative programming language whose programs can be verified, i.e. the implementation of the program can be rigorously checked against its logical specification for correctness, without ever running the code.

Programs are built from integers, booleans, bounded arrays, loops, and procedures that can return values, and their specifications quantify over program state with forall and exists. Verification covers not just partial correctness but termination too: loops and recursive procedures carry variant measures that prove they finish, giving total correctness. A verified program can then be compiled to a native executable.

Cavalry also runs in the browser — the whole pipeline, Why3 and Z3 included, compiled to JavaScript and WebAssembly with no server round-trip. For the theory behind Cavalry and Hoare logic, see my article.

Setup

You need OCaml >= 4.14 with opam, and Why3 driving the Z3 4.16.0 satisfiability-modulo-theories (SMT) solver, which discharges the verification proof obligations. From a checkout of the repository:

With Nix (recommended). The bundled flake (flakes enabled) provisions opam, the native libraries, and Z3:

nix develop

The first entry bootstraps a local opam switch, installs the dependencies, and runs why3 config detect so Why3 can find Z3; a stamp file guards this so it happens only once per checkout. With direnv, direnv allow enters the shell and bootstraps automatically.

Without Nix. Install Z3 4.16.0 yourself (e.g. brew install z3), then provision the switch and prover:

opam install --deps-only --with-test .
why3 config detect  # let Why3 find the Z3 prover

Usage

dune build
dune exec -- cav verify example.cav    # check the pre/postconditions hold
dune exec -- cav run example.cav       # interpret the program
dune exec -- cav compile example.cav   # compile to a native executable (gated on verification)
dune runtest                           # run the test suite

By default the prover reasons over unbounded (mathematical) integers. Pass --machine-int to verify — or --native-int to compile — to reason over OCaml's 63-bit machine integers instead, in which case every arithmetic operation must additionally be proven not to overflow.

Examples

The two examples below cover loops and recursive procedures; the rest — straight-line Hoare triples, returning values, arrays with forall/exists, booleans, division and modulo, and how a failed proof is reported — are in Cavalry by example. Each is a standalone program in assets/readme-snippets/snippets/; verify any of them with dune exec -- cav verify <file>.

Computing triangle numbers

A loop's invariant holds on entry and after every iteration, while its optional variant — a non-negative measure that strictly decreases each iteration — proves termination, giving total correctness.

Procedures, contracts, and recursion

A procedure is verified once against its contract: requires and ensures are its pre- and postcondition, and writes frames the globals it may modify. Callers — including the procedure itself, when it recurses — reason from the contract alone, not from the body. A variant that strictly decreases at each recursive call proves the recursion terminates, giving total correctness.