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. One colour is Aeneas-only: orange marks the translation stage, which Verus and blueprint projects do not have:

Atoms with a colour bar

Rust exec (Verus and Aeneas projects)

The bar uses the eight colours of the table below, a pure function of whether the Rust exec atom is tracked, whether it carries a translation-name, 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, no translation-name not translated — in scope, but Aeneas has not produced a Lean definition yet (Verus: no spec yet); empty bar = intent to verify
orange no verification-status, translation-name set translated — a Lean definition exists, but no spec theorem names it yet (Aeneas only)
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 in-scope Rust function that has no Lean counterpart yet (Aeneas: not translated; Verus: not specified); an orange bar means the translation exists and the spec is the missing piece; no bar at all means a pure-Rust project atom with no verification intent, for Rust projects alone.

White and orange are both "no status": the probe emits no verification-status until a spec theorem names the translation (probe-aeneas resolve_verification_status, hub P16/P24). Only translation-name tells them apart, so a consumer that reads verification-status alone sees one backlog bucket; the two colours split it into "not translated" and "not specified".

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 — not translated. In scope, no Lean definition yet (Verus: no spec yet) — the first half of the backlog.
  • orange — translated, unspecified. Aeneas has produced the Lean definition; no spec theorem names it yet — the second half of the backlog (Aeneas only).
  • 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 it is not part of the verification build, or the code explicitly opts it out (Verus #[verifier::external]; Aeneas @[out_of_scope]). The full lists are below. 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, an unmounted file (no mod chain from the crate's lib/bin roots reaches it, so rustc never compiles it), a bodyless declaration, 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. Missing a Lean translation is not by itself out of scope: a compiled function Aeneas has not yet translated is white backlog, not grey (P25); once translated it turns orange until a spec theorem names its translation.

Rust has two bodyless forms and both are grey, for the same reason: no body means nothing for Aeneas to translate, so no Lean definition, so no spec, so no status is ever possible. An extern "C" binding (untracked-reason: foreign-declaration) is implemented outside Rust entirely. A trait method declared without a default body (untracked-reason: trait-signature) has its proof obligations on the impls, which are tracked as their own atoms and colour normally. Trait methods with a default body are ordinary code and stay white, then orange once translated, until verified. Where Aeneas translates a trait declaration as an interface record, that atom carries a status and therefore stays tracked (P24).

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 the three chart categories:

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 eight bar / three dot colours, same exclusions) and cites this page as its spec; this page stays the canonical definition of the scheme. The orange bucket is counted from translation-name: a tracked atom with no verification-status is orange when it carries a translation-name and white when it does not.

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