veri

English | 日本語

A small foundation for formal verification in MoonBit, with reusable logical models and lemmas, implementations with contracts, and runtime differential checks.

QuickStart

To use a published release, add it to your own project:

moon add mizchi/veri

Add the import and proof setting to the consuming package's moon.pkg:

import {
  "mizchi/veri/bounds",
}

options("proof-enabled": true)

Put this code in digit.mbt. Like core Int::clamp, clamp includes both bounds. Use clamp_half_open(value, lower, upper) for an exclusive upper bound. Both functions require valid bounds; their proof preconditions are not runtime checks.

pub fn digit(value : Int) -> Int where {
  proof_ensure: result => 0 <= result && result <= 9,
} {
  @bounds.clamp(value, 0, 9)
}

test "clamp includes its upper bound" {
  assert_eq(digit(10), 9)
}

moon test --target js
moon prove

This minimal proof uses bundled Why3 and Z3 on PATH.

Documentation

Guide	Contents
Package index	Available models, APIs, and guarantees
Runtime APIs and graph checking	Map / Set, search, checked arithmetic, codecs, Union-Find, parsers, paths, and topology
Collections and arrays	Lists, stacks, queues, priority queues, trees, and FixedArray update contracts
Bitvectors and numeric models	Fixed-width bits, orders, number theory, reals, and rounding errors
Verification guide	Solver setup, moon prove, QuickCheck, and shrinking
Benchmarks	Core comparisons, measurement conditions, and tuning results
Proof architecture	Why3 / SMT-LIB bindings, runtime correspondence, and trusted boundaries
IEEE 754	Float / Double APIs, reference checks, proof scope, and limitations
Temporal model checking	moonx, Z3 / Apalache, and TaskGroup / lease-clock examples
Practical verification workflows	CI suites, saved counterexamples, model builders, and implementation comparisons

License

Apache-2.0.