Glossary

Terms used across VeriLib verification projects. Adapted from the VeriLib glossary.

Verification Statuses

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).

Atom Kinds

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

Kind	Description	Examples
Implementation	Executable code that can have specs attached	Rust functions, Verus exec-defs, Aeneas-generated Lean defs
Specification	Logical statements that define or prove properties	Verus spec-defs and proof fn, Lean theorem, lemma, non-translation defs

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

Verification Status

Applies to both implementation and specification atoms.

Status	Meaning
transitively-verified	Verified and all transitive dependencies are also verified or trusted
verified	Compiles successfully, all proofs discharged (but at least one transitive dep may be unverified/failed)
unverified	Has sorries, admits, or warnings
failed	Has compile errors
trusted	Axiomatically assumed (e.g., axiom, #[verifier::external_body])
null	Not subject to verification (test functions, constants)

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.

Specification Status

Applies to implementations only.

Status	Condition
specified	Has associated specs (specs list is non-empty)
unspecified	No associated specs (specs list is empty or null)

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

Color Mapping

Atom status colours — the bar/dot scheme and the tracked denominator — are defined canonically in Atom statuses and colours; the reference counter (colors.py) lives in veritooling.