Glossary

This document defines verification statuses for software verification projects across multiple proof frameworks (Rust only, Rust with Verus, Lean only, Rust with Lean and Aeneas).

Atoms are classified into two kinds based on their role in verification:

Key distinction: Implementations can have specifications attached to them. Specifications cannot—they ARE the specs.

Applies to both implementation and specification atoms.

The distinction between transitively-verified and verified is computed by probe enrich (reverse-BFS contamination over the dependency graph). probe-verus and probe-aeneas run this enrichment automatically as the last step of extract.

Applies to implementations only.

Specifications are always unspecified by definition—they cannot have specs attached to them.

Colors provide visual feedback based on verification progress. The scheme follows a progression from untracked to fully verified, with a separate branch for trusted/axiomatic items.

Verification scope: Green comes in two strengths depending on whether explicit contamination (unverified or failed) exists in the transitive dependency closure:

• Transitively verified (verification-status: "transitively-verified"): The function is verified and no transitive dependency is explicitly unverified or failed. Dependencies with missing verification-status (untracked Rust functions, spec functions) and dependencies absent from the atom map are transparent — they do not block transitive scope. Trusted (axiomatic) dependencies are also transparent.
• Locally verified (verification-status: "verified"): The function is verified, but at least one transitive dependency is explicitly unverified or failed.

Colors apply to Rust functions from the project under analysis — that is, atoms with language: "rust" and a non-empty code-path. Stubs with code-path: "" represent functions from external crates and are excluded from color assignment and counting.

The progression from least to most verified:

Purple (Trusted) indicates intentional axiomatic assumptions rather than incomplete work.

Spec validation note: All specs are currently considered validated if they appear in the JSON — to be present, the spec must be on main, meaning it passed PR review. Light Blue is kept as a placeholder for future spec-invalidation support; until then, all specified-but-unverified functions are Dark Blue.

Use scripts/count-colors.sh to count Rust project functions per color. Auto-detects probe-aeneas/extract and probe-verus/extract JSON:

scripts/count-colors.sh input.json

The script scopes to project functions (code-path != ""), excluding external crate stubs. Grey includes test functions. Grey, White, Yellow, Dark Blue, and Purple form a partition of the total; Green is an informational overlay within Dark Blue (verified subset of specified functions). Functions that are specified but not yet verified (unverified or failed) are counted in Dark Blue but not in Green.

Specifications skip Grey, White, Yellow, and Blue tiers — they ARE the specs. Only three colors apply:

Functions are Grey (untracked) — no formal verification framework is in use, so no verification will be performed.

Implementations (exec-defs):

In Verus, spec validation and proof happen atomically in a single verifier pass — you cannot have "specs validated but function not verified." Therefore Blue tiers (which represent the gap between spec authoring and proof) do not apply. Blue tiers are meaningful for Lean/Aeneas where spec authoring and proof are separable steps.

Specifications (proof fn, spec-defs):

Implementations (def with associated theorems):

Specifications (theorem, lemma, standalone def):

Aeneas translates Rust functions to Lean definitions, which can then be specified and verified.

Structure:

• Each Rust function → one Lean translation (def)
• A translation may call other translations (e.g., loop bodies)
• Each translation may have one or more specs (theorems)
• One spec is the primary spec; others are auxiliary lemmas

Status inheritance:

• A Lean translation is specified if it has a primary spec
• The Rust function inherits status from its Lean translation
• External function stubs → trusted (Purple)

Color assignment:

1. Should failed have its own color (red) distinct from unverified?
2. How to identify the "primary spec"? Options:
   • Naming convention (e.g., foo_spec for function foo)
   • Annotation system in Lean
   • First spec in declaration order
3. Should Translated use Yellow or Light Purple? Yellow distinguishes it more clearly from the Blue tiers; Light Purple groups it visually closer to Purple.
4. For Aeneas Rust atoms, is-relevant == !is-disabled (both derived from functions.json). is-disabled is the canonical field; should is-relevant be removed from Rust atom enrichment as redundant? See probe-aeneas#20.