Mica

A verified verifier for a fragment of OCaml, built in Lean 4 with Z3.

Example

Mica verifies OCaml functions against specifications written as annotations. Here is a recursive function that computes triangle numbers, verified against the exact closed-form spec r = n*(n+1)/2:

let rec triangle (n: int) : int =
  if n <= 0 then 0
  else triangle (n - 1) + n
[@@spec fun x ->
  assert (x >= 0);
  ret (fun v ->
    assert (v = x * (x + 1) / 2))];;

Build it and run it with:

$ lake build
$ lake exe mica Tests/recursion/recursive.ml
Status: all declarations verified

Examples/ is reserved for case studies: complete programs of independent interest, verified end to end. Everything else — small programs exercising one language or verifier feature — lives under Tests/, one directory per feature. Tests for new functionality go in Tests/, not Examples/.

How it works

Unlike approaches that generate a single verification condition and hand it off to an SMT solver, Mica maintains an interactive session with Z3. The verifier incrementally declares constants, asserts facts, and issues check-sat queries as it walks the program. It can also branch on the solver's responses — for example, testing whether a property is provable before deciding how to proceed.

The verifier is written in Lean 4 and comes with a mechanized correctness proof: if the verifier accepts a program, the program satisfies its specification with respect to a weakest-precondition semantics. Since the SMT solver exists outside of Lean, correctness is proved against an abstract characterization of the interactive session (push/pop, assert, check-sat) that captures what it means for the solver's responses to be sound.

The weakest-precondition rules are currently axiomatized and will be derived from the operational semantics in a future version.

Building

Requires Lean 4 and Z3 (on PATH for running the verifier).

lake build                   # build the verifier
lake run testsuite           # run the testsuite (Examples/ and Tests/)
lake exe mica <file>         # the main executable 

Project structure

Path	Description
Main.lean	CLI entry point for parsing, elaboration, printing, and verification
Mica/Frontend/	Lexer, parser, pretty-printer, spec parser, and elaboration from OCaml syntax to TinyML
Mica/TinyML/	Core language syntax, typing, printer, operational semantics, heap model, and weakest-precondition interface
Mica/FOL/	First-order logic syntax, semantics, substitution, deduction, and printing
Mica/Engine/	Generic infrastructure for interactive SMT sessions and drivers
Mica/Verifier/	Specification language, checking program expressions, and the verifier correctness development
Mica/Base/	Shared utilities
Examples/	Case studies: complete verified programs
Tests/	Small feature-targeted tests, organized by feature, with expected .out files
Testsuite.lean	The testsuite runner, invoked via lake run testsuite