Skip to content

Atom statuses and colours

The minimal, informative colouring scheme for atoms: for every colour it says where the information comes from. It covers Verus and Aeneas (Rust) projects and Lean projects, and is the mapping the Atomizer persists and the frontend renders from the atom verification-status field.

This scheme is VeriLib-specific (it is about how VeriLib presents atom statuses, not about any individual probe), so this page is the canonical spec for it. The reference implementation lives in veritooling as colors.py, which cites this page as its spec.

This page covers a single snapshot — what each colour means. Rolling these colours up into progress over time (summary stats, burn-up charts, the blueprint dependency graph) is a separate concern, documented in Verification progress metrics.

Two visual channels

An atom carries at most two independent signals:

Channel Where What it means Which atoms
Colour bar (bottom) Verification status is this item implemented and verified in the proof language? Rust exec + blueprint node atoms
Colour dot (top-right) Checking status does the tool accept the artifact? verification artifacts

"Verification artifacts" are Verus specs and proofs, and Lean defs and theorems. They get a dot, not a bar: the question for them is not "meets its spec" but "does it go through". The dot is for the proof-language atoms themselves; any atom whose status depends on Lean atoms — a Rust exec measured against its Lean translation, a blueprint node measured against its Lean binding — gets a bar.

The two channels split cleanly by language (per P20): language: "rust" (kind exec) and language: "blueprint" (node atoms) → bar; language: "verus" (Verus spec / proof) and language: "lean" (any Lean atom) → dot.

Optional classification (scheme / construction / correctness / security) is shown by border colour. It is not a status.

Kind — the top-left label

The label at the top-left corner is exactly the atom's kind field from the JSON, verbatim. Possible values:

  • Rust (Verus / Aeneas): exec, spec, proof
  • Lean: def, abbrev, class, structure, inductive, instance, opaque, quot, projection, axiom, theorem
  • Blueprint (probe-leanblueprint node atoms): blueprint-definition, blueprint-theorem

Colour bar

The status rides on a bar at the bottom of the atom. Two atom populations carry it: Rust exec atoms (Verus and Aeneas projects) and blueprint node atoms (language: "blueprint", one per blueprint/paper node, from probe-leanblueprint ≥ 0.6.0). Both answer the same question — is this item implemented and verified in the proof language? — so both use the same bar palette:

Atoms with a colour bar

Rust exec (Verus and Aeneas projects)

The bar uses the seven colours of the table below (white = an empty bar: unspecified, no spec yet), a pure function of whether the Rust exec atom is tracked and its verification-status (exactly what colors.py counts):

Bar JSON condition Meaning
grey untracked: true untracked — out of verification scope (see below)
white no verification-status unspecified — in scope, no spec yet (empty bar = intent to verify)
red verification-status: "failed" error — verification failed
yellow verification-status: "unverified" incomplete proof: a Lean sorry or a Verus assume()
light green verification-status: "verified" locally verified — meets its spec
dark green verification-status: "transitively-verified" verified, and so are all its dependencies
purple verification-status: "trusted" assumed correct (Verus #[verifier::external_body] / admit(), Lean axiom / *External.lean)

The bar is what makes white unambiguous: a white bar means an unspecified (in-scope, not-yet-specified) Rust function; no bar at all means a pure-Rust project atom with no verification intent, for Rust projects alone.

Blueprint node atoms

A blueprint node atom's verification-status is derived from its evidence — aggregated from the machine statuses of the Lean decls bound to the node, or capped at trusted for attested claims without checkable code (normative semantics: probe-leanblueprint SCHEMA.md). The bar is a pure function of verification-status and blueprint-node-class (the node's binding state, playing the role untracked plays for Rust):

Bar JSON condition Meaning
grey untracked: true untracked — the node is deliberately outside the formalization effort (see below)
white verification-status: "unverified" and blueprint-node-class: "planned-only" / "decl-missing" planned — no Lean decls linked yet (the formalization backlog)
red verification-status: "failed" error — a bound Lean decl fails to check
yellow verification-status: "unverified" and blueprint-node-class: "bound" in progress — bound to Lean decls with incomplete proofs (a sorry)
light green verification-status: "verified" all bound Lean decls locally verified
dark green verification-status: "transitively-verified" all bound Lean decls verified, and so are all their dependencies
purple verification-status: "trusted" attested, not machine-verified — trusted-reason: "upstream-proved" (Verso renderer proved the binding in a dependency) or "declared" (a human \leanok claim)

Grey follows the same rule as Rust: tracked by default, out of scope only by explicit declaration. Every blueprint node is tracked — appearing in the blueprint is the default declaration of intent — and leaves the tracked set only when the project explicitly marks it out of the formalization effort: prose-only background material, results consumed from the literature, statements whose formalization deliberately takes a different route (FLT's nolean-* nodes are the pattern). Neither blueprint format has a native marker yet, so the declaration comes from curation (as with Aeneas's config out-of-scope entries), and no emitter sets untracked: true on node atoms as of probe-leanblueprint 0.6.0 — greys appear once that support lands. The denominator mirrors Rust: #tracked = all node atoms − grey. Two more rules for this population:

  • Count the Lean and blueprint layers separately. A bound node atom's bar mirrors Lean decls that already carry their own dots (dependencies names them; the Lean atoms point back via blueprint-label) — summing across the layers double-counts.
  • Purple keeps its bar-channel meaning — the trust base: the claim is attested (by the Verso renderer or a human) rather than machine-verified, and trusted-reason says which.

Colour dot — verification artifacts

The status rides on a dot at the top-right corner of the artifact, a pure function of verification-status:

Verification artifacts with a colour dot

Dot JSON condition Meaning
red verification-status: "failed" fails to check
yellow verification-status: "unverified" checks, with an incompleteness warning (sorry / assume)
green anything else ("verified" / "transitively-verified" / "trusted" / none) accepted by the tool

red/green are always from the build/verify command. Yellow is from the command for Lean, but from the probe's source scan for Verus.

Legend (Verus / Aeneas)

What a Rust function's bar colour means, in plain words:

  • grey — not tracked. Deliberately outside the verification effort; ignored in every count.
  • white — unspecified. In scope, no spec yet — the work backlog.
  • red — broken. Has a spec; verification errors out.
  • yellow — in progress. Has a spec; the verification is incomplete (a sorry / assume()).
  • light green — verified. Verified against its spec.
  • dark green — verified end-to-end. Verified, and so is every dependency.
  • purple — trusted. Deliberately assumed, not verified — the trust base.

Tracked = every Rust function that is in verification scope = all bar colours except grey. Every Rust function is tracked by default; one leaves the tracked set only when the code explicitly marks it out of scope (Verus #[verifier::external]; Aeneas untranslated or @[out_of_scope]). Progress is #verified / #tracked, and a project is done when every tracked function is green or purple (verified/transitively-verified, or trusted).

Tracking and the denominator

Every Rust function is tracked by default (white bar). Out-of-scope is stated explicitly in the code and read by the probes:

  • Verus — #[verifier::external], cfg-inactive code, or an external-crate stub → untracked: true → grey.
  • Aeneas — cfg-inactive code, a non-library target (build.rs, tests/, examples/, benches/), a Lean-side @[out_of_scope] annotation on the translation, or a curated config out-of-scope entry → untracked: true → grey. Absence from functions.json alone is not out of scope: a compiled function Aeneas has not yet translated is white backlog, not grey (P25).

This gives a well-defined denominator, so we can report

#verified / #tracked      where #tracked = all exec atoms − grey (untracked)

Excluded from every count (both channels), before any colouring: external-crate stubs (empty code-path) and editorial/auto-generated exclusions (is-hidden / is-ignored / is-extraction-artifact). These are not atoms the project owes work on, so they never enter the bar or dot totals.

Counting: colors.py

The scheme above is implemented by veritooling's colors.py, the reference colour counter. It reads a probe extract JSON (probe-verus, probe-lean, or probe-aeneas — auto-detected from the schema field) and emits the per-colour counts for both channels plus the progress summary and chart frontiers:

colors.py <extract.json>          # metric record as JSON
colors.py <extract.json> --table  # human-readable table

colors.py is a straight implementation of the tables above (same two channels, same seven bar / three dot colours, same exclusions) and cites this page as its spec; this page stays the canonical definition of the scheme.

colors.py does not yet read probe-leanblueprint/extract files; when it (or any counter) does, blueprint node atoms form their own bar population (same seven colours and the same tracked = all − grey denominator as Rust — see Blueprint node atoms), never merged into the Rust bar or Lean dot totals.