Proof Explorer
604 proof sessions (397 beyond derived Clone impls)2,722 prover leaves4 provers: alt-ergo 2,414, z3 285, cvc5 22, cvc4 189.3 s recorded prover time4,992 obligations
Loading the proof explorer. This panel needs JavaScript. If it does not appear, your browser may have it disabled.
The recorded proofs of krabka-verified at broker
commit ad5dcb0933ea,
one session per function, with the browser re-check when the build carries Why3 and the browser provers.
A session is what why3find records when it proves one function.
Creusot translates the Rust into a Coma program, Why3 derives one verification condition per vc_ goal, and why3find tries the configured provers on each
goal, splitting it with split_vc or normalising it
with compute_specified when no prover discharges it whole. The
session stores that tree: per goal, which tactic split it, and for each leaf which prover proved it and
in how many seconds. The explorer shows the trees as recorded in the repository.
An obligation is one condition inside a goal, named by
the [@expl] label Creusot attaches when it generates it: a
precondition at a call site, a postcondition at a return, a loop invariant on entry and after each
iteration, an integer overflow, a division by zero, an index in bounds. Each label carries the Rust
source span it came from, so every row below links to the line the condition is about.
Proof sessions
Kernels are the decision functions the broker calls, helpers and lemmas support their proofs, and derived
impls are the 207 Clone implementations Creusot
proves alongside; those are hidden until you turn the chip on. Pick a session for its proof tree, its
obligations, the generated Coma, and the browser re-check. A link of the
form #session=module/name opens a session directly.
Toolchain. Creusot v0.13.0;
why3find with provers alt-ergo, z3, cvc5, cvc4,
tactics compute_specified, split_vc, time
limit 5 s per prover call (fast path 0.2 s), split depth 6.
Sessions synced from krabka-io/krabka-broker@ad5dcb0933ea on 2026-10-15.
What this page can and cannot do. The sessions are the repository's recorded proofs, shown as why3find stored them; nothing here re-derives them. The browser re-check, when the build includes it, replays the recorded tactics through Why3 and sends each supported leaf to its recorded prover: Alt-Ergo in JavaScript, or Z3, cvc5 and CVC4 in WebAssembly. These use the solver versions pinned by Creusot and Why3's prover-specific SMT-LIB drivers. Z3 enables shared memory with a one-time page reload and resumes the check. A browser timeout does not invalidate the recorded proof: browser performance and budgets differ from native CI.