[ Bounded · Invariant · Logic ]

Write the specification.
Check it.

bil is a statically typed language for writing a specification next to its implementation and checking that they agree. It has guarded commands (if … fi, do … od), refinement, first-order logic, and system models of concurrent state machines. Checks run through weakest preconditions, the built-in bil-smt solver or Z3 (with proof certificate checking), and an explicit-state model checker. It can also emit Verus code.

View on GitHub → White paper Semantics

$ cargo run -- verify examples/gcd_refinement.bil

examples/gcd_refinement.bilexcerpt

do x = a, y = b
  invariant x > 0 && y > 0
            && gcd_val(x, y) == gcd_val(a, b)
  variant   x + y
:
  x > y -> x := x - y
[] y > x -> y := y - x
od

[PROVED (by z3)] refinement of gcd_spec
[BOUNDED (6561 samples)] invariant preservation

§1

What the name means

Each word in the name maps to a part of the language.

Bounded

Proved or sampled, and it says which

Each proof obligation is reported as PROVED (Z3 with a checked proof certificate, or built-in bil-smt) or BOUNDED, with the number of samples tried. bil verify exits 1 when a result is only BOUNDED, unless you pass --allow-bounded.

Invariant

Conditions that must keep holding

A loop has an invariant and a variant. A system has invariants that must hold in the initial state and after every transition. A violation is reported with the shortest trace that reaches it.

Logic

First-order logic and types

Conditions use forall and exists. concept hierarchies (<:) are checked for cycles and used as types, with Hindley–Milner inference. Either ASCII or Unicode works: => or ⇒, forall or ∀.

§2

How a program is processed

A program is converted to three intermediate representations (IRs) in turn. Specification code (spec, requires, ensures, invariant, variant) is removed in the last one, so it is not in the code that runs. bil dump-ir prints each level.

.bil

Concepts, axioms, specs, fn, proof, system.

→

HIR

Resolved types, flattened concept inheritance, desugared |> pipelines.

→

VIR

Marks each node as spec, proof or exec. Holds the verification conditions and system transitions.

→

verify

wp · z3 · bil-smt

model-check

BFS · LTL

emit-verus

step_i · next

vm · build

from LIR

§3

Example: source and output

The source is from examples/. The output is copied from the CLI, with lines cut where marked.

examples/gcd_refinement.bilrefinement

spec gcd_spec(a: Int, b: Int) -> Int
  requires a > 0 && b > 0
  ensures  result > 0 && (a % result == 0)
           && (b % result == 0) && …

fn gcd(a: Int, b: Int) -> Int
  refines  gcd_spec
  requires a > 0 && b > 0
  ensures  …
=
  do x = a, y = b
    invariant x > 0 && y > 0
              && gcd_val(x, y) == gcd_val(a, b)
    variant   x + y
  :
    x > y -> x := x - y
  [] y > x -> y := y - x
  od
  then x

$ bil verify examples/gcd_refinement.bilexcerpt

[PROVED (by z3)] fn `gcd_val` — if..fi Guard Totality
[PROVED (by z3)] fn `gcd` — Refinement Weakened Precondition
[PROVED (by z3)] fn `gcd` — Refinement Strengthened Postcondition
[BOUNDED (81 samples)] fn `gcd` — do..od
    Invariant Initialization (Pre => I)
[BOUNDED (6561 samples)] fn `gcd` — do..od
    Invariant Preservation Branch #1 (I ∧ G1 => wp(S1, I))

The refinement is proved. The loop invariant is only sampled.

examples/mutex_protocol.bilsystem

system PetersonMutex {
  state p0: Phase = Idle
  state p1: Phase = Idle
  state turn: Int = 0

  invariant MutualExclusion:
    !(p0 == Critical && p1 == Critical)

  temporal StarvationFreeP0:
    (p0 == Trying) ~> (p0 == Critical)

  transition
    p0 == Idle -> p0 := Trying, turn := 1
  [] p0 == Trying && (p1 == Idle || turn == 0)
       -> p0 := Critical
  [] …
}

$ bil model-check examples/mutex_protocol.biloutput

States explored: 10 | Transitions fired: 16
Max depth: 3 | Max nondeterministic branching: 2
[LTL PROVED] temporal `StarvationFreeP0`
[LTL PROVED] temporal `StarvationFreeP1`
[VERIFIED] All safety invariants, LTL temporal
           properties, deadlock-freedom (BB),
           and variant bounds hold.

For a violation, see seeded_bugs/spe_late_cutoff.bil: model-check prints a 14-step trace.

§4

Commands

One binary. Run any of these from a checkout with cargo run --.

Command	What it does
check	OntoLogic DAG, contradiction linter and Hindley–Milner type check.
solve	Z3 / CVC5 / `bil-smt` ontology consistency and subsumption (`--subsumes C P`).
verify	Dijkstra weakest preconditions, refinement and `proof` lemmas. Bounded, Z3 (proof-checked) and built-in `bil-smt`.
model-check	Explicit-state search with LTL (`~>`, `eventually`), deadlock freedom and timed `deadline`s. `--bmc` for symbolic.
run · vm · build	Tree-walk interpreter, bytecode VM on ghost-erased LIR, standalone native binary.
emit-verus	Verus Rust. A `system` becomes a `step_<i>` function per transition plus a `next` relation.
dump-ir	Inspect HIR → VIR → LIR.
all · repl	check + verify + model-check + run in one go; interactive REPL.

§5

What `emit-verus` proves, and what it does not

For each system, emit-verus writes one function per transition. Verus then checks each function.

Proved

Every step_<i> function keeps the system's invariants true: if they hold before the step, they hold after it.
All 14 examples/domains systems emit Verus that verifies.
Verus rejects the 6 seeded safety bugs with “postcondition not satisfied”.

Not covered

Liveness (“this eventually happens”, written ~> or eventually). Only model-check checks these.
Wrong axioms. An axiom is assumed true and never proved.
That your own Rust code matches the next relation. You prove that yourself.

Of the 11 seeded bugs, Verus is expected to reject 6. The other 5 are listed with reasons in tests/verus_emit.rs: 2 break a liveness property and 3 are wrong-axiom bugs that the model checker does not see. Verus version: 0.2026.10.26.d17fbd0. Numbers inside the example models are illustrative.

§6

Example systems

Models in examples/domains/. The seeded-bug files are copies with one fault added.

14domain systems that emit verifying Verus

11seeded bugs; the test suite checks each is caught

6of those are also rejected by Verus

83%line coverage (CI floor is 78%)

aerospace envelope automotive ACC anti-windup PI zero-trust BMS balancing MQTT QoS 2 press cell infusion pump geofence reactor safety traffic and rail cobot cell semiconductor SPE surgical teleop

These are models, not certified safety cases. Sources for domain details are in CITATIONS.md.