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. Every progress chart — the Rust bar-channel chart and the Lean charts alike — draws the same three categories: tracked, in-progress, and completed. The probe families differ in only one way: the unit they count, which is a Rust exec atom, a Lean declaration, or a blueprint node.

The three categories

Category Definition Colour
tracked in verification scope — the ceiling all bars − grey
in-progress verification-status: "unverified" — a spec exists, the proof is incomplete (a sorry or assume) yellow
completed verification-status: "verified" + "transitively-verified" + "trusted" light + dark green + purple

Two properties are worth stating explicitly, because they differ from a stacked percentage chart:

  • tracked is the ceiling, and the invariants are tracked ≥ completed and tracked ≥ in-progress.
  • in-progress and completed are disjoint but do not sum to tracked. The remaining gap holds the units that are neither: unspecified (white) and failed (red).

Verus and Aeneas (bar channel)

Two artifacts sit here, Verus and Aeneas. The snapshot partition is a bar-channel metric, because it rests on the tracked denominator. Their stats derive from the seven bar colours that colors.py counts.

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)

If we want to display a summary per bucket, we have five buckets which 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" — the chart's completed light + dark green
trusted verification-status: "trusted" purple

Progress chart (burn-up over time)

The chart draws the three categories as cumulative curves rather than a stack to 100%:

tracked ≥ completed        tracked ≥ in-progress

The unit is the Rust exec atom, and tracked is the ceiling from the partition above, so a project is done on the chart when completed meets tracked.

Lean and leanblueprint (dot channel)

Lean has no exec side, so there is no colour bar and no fixed tracked denominator; tracked here is a count of units that moves over time (see the caveats below). 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 three categories as the bar-channel chart.

One plot per project (definitions and theorems pooled)

A Lean project gets a single panel, with definitions and theorems pooled into one series per category. plot_progress.py writes one burnup.svg, and the same file serves both the per-project page and the cross-project dashboard.

Pooling is safe because the three categories apply uniformly to both kinds: a definition is completed when its body is sorry-free and checks, a theorem when its proof is.

Pipelines (what each category counts)

Which pipeline applies is set by whether the project ships a blueprint:

Pipeline Served by Unit tracked in-progress completed
Plain Lean (no blueprint) probe-lean Lean declaration every declaration: no fixed ceiling, it grows with the project the project's full sorry count, since every declaration is counted sorry-free declarations that verify
leanblueprint probe-leanblueprint blueprint node every blueprint node: a per-sample inventory, so it 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) nodes that are sorry-free per probe-lean's verification-status, not a hand-toggled \leanok

Two Lean-specific caveats follow from that table. tracked is not a fixed ceiling the way it is for Rust, so the Lean chart is not a strictly monotonic burn-up: for plain Lean the ceiling rises as declarations are added, and for leanblueprint it can fall when the blueprint inventory shrinks. And on the blueprint side the unspecified gap has a concrete meaning — nodes with no formalized statement yet.

The VeriLib team can run these scripts from veritooling as-is or adapt them; only the output shape above is 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.