The panic that provably cannot happen

Assertions

The checks rustc already inserts, answered before codegen

Rust emits a bounds test, an overflow test and a division guard for the code you write, and panics if one fails. Keller-Verify reads the optimised MIR where those assertions live, turns each one into an integer formula under the guards that reach it, and asks whether the failure condition is satisfiable.

Two properties decide how much a verdict is worth. The analysis is path-sensitive, so each branch condition is folded in before the solver is asked: if x < 100 { x + 1 } is proved, if x < 200 { x + 100 } is a counterexample at x = 192, and a value merged from two branches stays one-of-them rather than being narrowed to one. And a witness names only what the obligation forces: the operands of the failing operation, plus any symbol the solver proves is pinned, so a value the model merely chose is not printed as evidence.

A report also states what it did not check. The coverage headline — reachable, supported and unsupported assertions, plus decided and unmodelled panic sites — appears in the console, the --json summary, the HTML report and the SARIF log's run properties, so a gap cannot be inferred away from an empty findings list.

Pipeline

Where the proof happens

Every rustc invocation is a separate process and several run at once, so each one files its findings under its own crate and the top-level command merges them. Exit codes separate the two failures a CI job needs to tell apart: 1 is a counterexample, 3 is a crate that did not compile or a setup that could not run.

$ cd tests/safe_code && keller-verify keller verify
[PASS] Verified formal integrity: main (bb10)
[PASS] Verified formal integrity: main (bb12)
    Total assertions checked: 2
    PASS: 2   FAIL: 0   WARN: 0

$ cd tests/branch_merge && keller-verify keller verify
[FAIL] Arithmetic Overflow Detection (Add) -> Exploit path found! [_3 = 255, 100_u8 = 100, flag (_1) = true] in bump (bb3)
    Total assertions checked: 1
    PASS: 0   FAIL: 1   WARN: 0
[Keller-Pipeline] Verification FAILED: report.json contains FAIL events.

Excerpted: startup banners, the box rules around each summary block and the repeated per-crate blocks are omitted, and the result lines are verbatim.

Evidence

A verdict you can hand to someone else

Every verdict, a PASS included, writes the formula it was decided from as SMT-LIB, so the answer can be checked without trusting the tool. Each crate also gets an index.json manifest listing every obligation the run emitted — proofs included — with the status, kind, source location and artifact name, sorted so two runs of unchanged code produce byte-identical bytes. This one is from tests/branch_merge: the header names the crate, function, block and verdict, the ; reachable: line is the guard that leads to the block, and the ; witness: lines are the values read back from the model. Handed to Z3 on its own, the file answers sat.

; keller-verify proof obligation
; crate:    branch_merge
; function: bump
; block:    bb3
; kind:     overflow
; verdict:  FAIL (sat)
; reachable: (or (= mir_1 0) (not (= mir_1 0)))
; witness:  overflow_l = 255 (_3)
; witness:  overflow_r = 100 (100_u8)
; witness:  mir_1 = true (flag (_1))
(declare-fun phi_bb3_2 () Int)
(declare-fun overflow_l () Int)
(declare-fun overflow_r () Int)
(declare-fun mir_1 () Int)
(assert (= overflow_l phi_bb3_2))
(assert (= overflow_r 100))
(assert (or (> (+ overflow_l overflow_r) 255) (< (+ overflow_l overflow_r) 0)))
(assert (or (= mir_1 0) (not (= mir_1 0))))
(assert (or (and (= mir_1 0) (= phi_bb3_2 0)) (and (not (= mir_1 0)) (= phi_bb3_2 255))))
(assert (>= mir_1 0))
(assert (<= mir_1 1))
(check-sat)
sat

The encoding is unbounded integer arithmetic, which is why the u8 range is asserted rather than implied by a bit-vector width. The merged value is a phi symbol defined by a disjunction, one of these values, chosen by the branch that was taken; writing it as an if-then-else instead would drop the other branch's value. On sat the same values are asserted into a second file, bump_bb3.witness.smt2, which must also answer sat, so the counterexample is checkable too.

A proof is checkable as well: a PASS writes PASS (unsat), which must re-discharge to unsat. keller explain <FILE> describes an obligation, and keller replay <FILE> compares fresh Z3 output with the verdict recorded in its header, rejecting a mismatch or invalid SMT-LIB. The executed trust checklist runs those checks against this tree.

The repository's tests/ directory holds the fixture crates the shell runner drives (tests/run_tests.sh, the step the workflow's fixture job runs — the workflow is in the tree, and no run of it has been observed from a checkout, so the gate that is shown is the local one), and each case's whole report.json is compared against a committed golden, so a change to a verdict, a witness, a class or a source location fails the suite rather than waiting for a reader to notice.

Limits

What it does not do

What this build does not do is listed below. The short version:

• Every verdict describes a debug build, because that is where rustc emits the assertions. A release build wraps instead of panicking, so "cannot overflow" and "will not abort" are different claims.
• It removes no runtime check and proves no whole program. An empty report means none of the checks this tool performs can fire, not that the code cannot panic.
• A loop is unrolled to a bounded number of trips; past that, a loop-carried value is widened to its type's range rather than kept exactly.
• Integer bit-twiddling and narrowing casts are not modelled, so a value out of one becomes a free symbol bounded by its type. Division guards are checked on the divisor and on MIN / -1; the quotient itself is not propagated, so a value derived from it also becomes a free symbol.
• There is no cross-function reasoning, and third-party dependencies are not analysed.
• An obligation the encoder cannot express, or the solver cannot decide, is reported as a WARN rather than skipped, and a function whose dataflow stops converging is recorded as path-insensitive with a note saying which of its verdicts to distrust.

Get started

Build it once, run it from the crate you are checking

It drives cargo check, so it needs the pinned nightly with rustc-dev and a Z3 4.16.0 install. The verifier selects the compiler it was built against, so a project pinned to its own toolchain is still analysed. The usage guide has every flag, the exit codes and the roll-out recipe for a codebase that is not clean yet.

git clone https://github.com/KELLERBABG/Formal-Verification.git
cd Formal-Verification
cargo build                       # needs Z3 and a nightly with rustc-dev
cd /path/to/your/crate
/path/to/Formal-Verification/target/debug/keller-verify keller verify

# gate only on findings this change introduced, and annotate the pull request
keller-verify keller verify --baseline .keller-baseline.json --sarif keller.sarif

This is a prototype rather than a supported product: it is dual-licensed MIT or Apache-2.0, the supported install baseline is Ubuntu 24.04 with nightly-2026-07-24 and Z3 4.16.0, and the security policy treats a wrong PASS as the bug class worth reporting. Both are in the repository.

A tagged release archive bundles the executable, Z3 and a launcher, but it is not a static binary: it resolves the pinned toolchain at run time, and the build embeds the exact rustc release and commit, so a run refuses a different compiler. The packaging workflow is in the tree, but no run of it has been observed from this checkout — the checks shown here are the local ones.