Skip to content

Verification progress metrics

This page describes how VeriLib turns the atom colour scheme into progress over time: the summary stats and burn-up charts rendered by veritooling's verification-progress-history tool. The colour vocabulary itself is defined on the Atom statuses and colours page. That vocabulary covers the bar and dot channels, the seven bar colours, and the tracked denominator. This page is about counting those colours and plotting them.

The burn-up is drawn in a vocabulary that is unit-parametric. The same six frontiers drive both the Rust bar-channel chart and the Lean burn-ups: tracked, verified+trusted, verified, in-progress, unspecified, and failed. The probe families differ in only two ways. The first is the unit they count, which is a Rust exec atom, a Lean declaration, or a blueprint node. The second is whether they have a tracked ceiling.

Verus and Aeneas (bar channel)

Two artifacts sit here, Verus and Aeneas. The snapshot partition and translated are bar-channel metrics, because they rest on the tracked denominator. Their stats derive from the seven bar colours that colors.py counts, and translated additionally uses the Aeneas translation-name field.

Throughout, #exec means the Rust exec atoms that survive the exclusions on the scheme page: an empty code-path, or the is-hidden, is-ignored, or is-extraction-artifact flags.

Summary (snapshot partition)

The five buckets are disjoint and sum to tracked:

Stat Definition Colour
tracked #exec − #untracked = unspecified + failed + in-progress + verified + trusted all bars − grey
unspecified no verification-status white
failed verification-status: "failed" red
in-progress verification-status: "unverified", a sorry or assume yellow
verified verification-status: "verified" + "transitively-verified" light + dark green
trusted verification-status: "trusted" purple
translated non-disabled exec atoms with a non-null translation-name, Aeneas only n/a

translated is not part of the partition. It is a milestone that cuts across the partition, since a verified Aeneas function is also translated.

Progress chart (burn-up over time)

The chart draws cumulative, nested curves rather than a stack to 100%:

tracked ≥ translated ≥ verified          (translated line: Aeneas only)
  • tracked is the ceiling, the upper bound.
  • verified is the proved frontier.
  • verified + trusted is the completion frontier. This is what reaches the ceiling at "done", where done means every tracked function is green or purple. trusted is drawn as its own band on top of verified, so the purple gap stays visible instead of being folded into verified, and you can see how much rests on axioms.
  • translated, for Aeneas, is the intermediate milestone between "in scope" and "verified".

in-progress and unspecified are not part of the default frontier set, because both are transient. A function leaves in-progress the moment its sorry or assume is discharged, and it leaves unspecified once it gets a spec. On a burn-up they therefore only ever shrink, and they already show up as the gap between the completion frontier and the ceiling. By default they stay summary slices.

They can still be drawn as optional overlay curves when the shrinking gap is itself what you want to watch. The burn-up tooling exposes them behind the --in-progress and --unspecified flags:

  • in-progress is the yellow count: an incomplete proof, a sorry or assume(false), which carries verification-status: "unverified".
  • unspecified is the white count: in scope, but with no verification-status yet. For Aeneas this is a function that is either not yet translated, or translated but with no spec-theorem yet.

These are distinct states, so the gap white + yellow + red must not be read as the sorry count. Each optional curve isolates one slice of it.

One invariant must hold. For Aeneas it is tracked ≥ translated ≥ verified. For Verus the translated line does not apply, so the invariant is just tracked ≥ verified.

Lean and leanblueprint (dot channel)

Lean has no exec side, so there is no tracked denominator and no colour bar. Every Lean atom carries only the coloured dot, red, yellow, or green from lake build, per the dot table. Lean still gets progress numbers and burn-up charts from the same verification-progress-history tool: it counts a unit (a Lean declaration or a blueprint node) and rolls the dot statuses up into the same burn-up vocabulary as the bar-channel chart. No tracked ceiling applies.

Two independent choices shape the output:

  1. the pipeline (plain Lean vs leanblueprint), set by whether the project ships a blueprint — this fixes which frontiers each panel draws;
  2. the view (split vs combined) — this fixes how many panels there are.

Pipelines (which frontiers)

Pipeline Served by Unit Per-unit metrics Ceiling in-progress means
Plain Lean (no blueprint) probe-lean Lean declaration total; without sorry (= verified + transitively-verified + trusted); trust boundary (= transitively-verified + trusted); failed none — total grows with the project the project's full sorry count, since every declaration is counted
leanblueprint probe-leanblueprint blueprint node formalized (statement/signature exists); proved (theorems only, sorry-free, confirmed by probe-lean's verification-status, not a hand-toggled \leanok) per-sample inventory — can fall as well as rise only formalized nodes whose bindings hold a sorry; a sorry in a declaration the blueprint doesn't track is invisible (veritooling #34)

Views (how many panels) — what the backend renders

Both pipelines can emit the burn-up in two layouts. This is the choice the VeriLib backend makes per surface:

View Command Output file Layout Render it for
Split by kind (canonical, default) plot_progress.py burnup.svg two panels — one for definitions, one for theorems the per-project page
Combined plot_progress.py --combined burnup-combined.svg one pooled panel (defs + thms) the cross-project dashboard
  • Per-project page → split (more informative). For leanblueprint the two kinds do not share an axis: a definition carries only formalized, a theorem adds proved. Pooling them would collapse the proved axis, so a rising line could no longer be read as more statements written vs more proofs closed — the two things worth telling apart. For plain Lean both panels draw the same three frontiers, total ≥ without sorry ≥ trust boundary, so the split just separates definition sorries from theorem sorries.
  • Cross-project dashboard → combined (aligns better). One curve per project is what a dashboard wants, and the pooled series lines up across projects. --combined writes a distinct burnup-combined.svg, so it never overwrites the split default. Note the leanblueprint ceiling is a per-sample inventory, so the combined curve can fall as well as rise; it is not a strictly monotonic burn-up.

The VeriLib team can run these scripts from veritooling as-is or adapt them; only the two output shapes above are contractual. For the exact metric definitions and the worst-status rollup, see veritooling's leanblueprint-metrics.md; for the plotting itself, the burn-up guide. The colour vocabulary they reuse is defined on the Atom statuses and colours page.

Blueprint dependency-graph colours

For a leanblueprint project the same tool also renders the blueprint dependency graph, with one node per blueprint-label. The node colouring extends the colour scheme with two signals that the native leanblueprint and Verso graphs cannot show:

  • machine-verified, drawn as solid green, means probe-lean's verification-status rollup for the node lands on verified rather than on a hand-toggled \leanok.
  • mismatch, drawn as a red outline, means the blueprint claims the node is proved but the machine refutes it. This is near-zero on code-derived Verso blueprints; the signal appears on \leanok-driven Massot blueprints.

The cross-project dashboard shows the blueprint's own claimed fully-proved fraction beside the stricter machine-verified rollup. Trust detection is node-local, so a green node that depends on an axiom in another node still reads verified. See the graph & dashboard guide.