Probe ecosystem¶
Probes are the tools that turn a source repository into atoms — the graph of declarations, dependencies, and verification statuses that everything else in VeriLib displays, counts, and certifies. The platform treats them as black boxes it shells out to, but they are a documented, versioned system with a machine-checkable interchange contract.
This page is the map. The atomizer and the cert workers are two different consumers of the same contract.
The contract repo¶
probe is not a probe. It is the hub that defines what every probe must emit and provides cross-tool operations over the results:
| Artifact | Role |
|---|---|
docs/SCHEMA.md |
The Schema 3.0 interchange spec — core fields, common optional fields, code-name conventions |
schemas/atom-envelope.schema.json |
JSON Schema (draft 2020-12) validating both single-tool and merged envelopes — the machine-readable contract |
probe CLI |
merge, enrich, summary — cross-tool operations |
probe-extract-check |
Validator that checks extract JSON against the source code it came from |
docs/consumer-guide.md |
Start here if you are writing a consumer |
The four extract probes¶
| Tool | Language | What it extracts | In the platform |
|---|---|---|---|
| probe-rust | Rust | Call-graph atoms from a SCIP index | Not wired into ATOMIZER_LANGUAGES |
| probe-lean | Lean 4 | Call graph + sorry detection + specs | Yes — Lean |
| probe-verus | Rust / Verus | Call graph + specs + verification status | Yes — Rust |
| probe-aeneas | Rust + Lean | Cross-language merged graph for Aeneas projects | Yes — Aeneas |
Each has docs/USAGE.md (command reference) and docs/SCHEMA.md (language-specific fields) in its own repo. All four run the same way:
probe-rust extract <project_path>
probe-lean extract <project_path>
probe-verus extract <project_path>
probe-aeneas extract <project_path> # needs aeneas-config.yml at the project root
Output lands in .verilib/probes/ — which is exactly where the atomizer's parsers look for it.
probe-rust is documented but not deployed
probe-rust is a first-class member of the interchange family with its own USAGE.md and SCHEMA.md, but the atomizer's plugin registry and ATOMIZER_LANGUAGES default (Rust,Lean,Aeneas) do not include it — "Rust" there means probe-verus. Plain-Rust extraction is available as a tool, not as a platform language.
The blueprint enrichment probe¶
probe-leanblueprint is not an extract probe — it is an enrichment layer on top of probe-lean. It reads a probe-lean atom base, augments each atom with blueprint-* fields carrying two-axis progress (statement status and proof status) from either the Verso Blueprint or the Massot leanblueprint ecosystem, and re-emits an enriched Schema 3.0 envelope alongside the extract probes in .verilib/probes/.
Since 0.6.0 the enriched envelope carries a second atom layer: one
language: "blueprint" node atom per blueprint/paper node (keyed
probe:blueprint:<label>, kind blueprint-definition / blueprint-theorem),
mirroring the blueprint's node set one-to-one. Node atoms carry a derived
verification-status — aggregated from the bound Lean decls' machine statuses,
or capped at trusted for attested claims — plus node-to-node uses edges
forming the paper graph. Enriched Lean atoms are byte-identical to what
probe-lean emitted; consumers read one layer per view (code-level stats →
language: "lean"; blueprint progress → node atoms; never summed). Rendering:
Atom statuses and colours (blueprint node atoms
use the colour bar).
Command reference and the full blueprint-* field set live in its own docs/USAGE.md and docs/SCHEMA.md.
Other repos in the family¶
probe-blueprint-classic, probe-blueprint-verso, and probe-vcvio share the probe- prefix but ship no docs/ directory and are not part of the Schema 3.0 extract/enrich contract described here.
Unknowns
Whether the blueprint-classic/verso and vcvio probes emit Schema 3.0 envelopes, and whether any are intended for platform integration, is not documented upstream. Treat them as research tools until their repos say otherwise.
Schema 3.0 envelope¶
Every probe emits the same outer shape:
{
"schema": "probe-verus/extract",
"schema-version": "3.0",
"tool": { "name": "probe-verus", "version": "0.1.0", "command": "extract" },
"source": { "repo": "…", "commit": "…", "language": "rust", "package": "…" },
"timestamp": "2026-03-17T12:00:00Z",
"data": { "…": "code-name → atom" }
}
For merged files (probe-aeneas), source is replaced by inputs — an array of provenance entries, one per input file.
data is keyed by code-name, a URI like probe:curve25519-dalek/4.1.3/scalar/Scalar#add(). The dictionary is a directed graph: keys are nodes, each atom's dependencies array holds the edges.
Core fields (every atom, every tool)¶
| Field | Type | Notes |
|---|---|---|
display-name |
string | Human-readable name |
dependencies |
array | Code-names of referenced atoms |
code-module |
string | Module / namespace path |
code-path |
string | Relative file path; empty for stubs |
code-text |
object | { "lines-start": N, "lines-end": N }; both 0 for stubs |
kind |
string | Language-specific declaration kind |
language |
string | rust, lean, or latex |
Common optional fields¶
| Field | Emitted by | Notes |
|---|---|---|
verification-status |
verus, lean, aeneas | transitively-verified, verified, failed, unverified, trusted |
trusted-reason |
verus, lean | Only when status is trusted (e.g. axiom, external-body) |
primary-spec |
verus, lean | Spec text in Verus; a code-name in Lean |
specs |
lean | Code-names of theorems that spec this atom |
untracked |
verus, rust, aeneas | Function is out of verification scope |
Renamed in Schema 3.0
untracked was called is-disabled in Schema 2.0 — same semantics (untracked: true = out of verification scope). This rename is the one breaking change in the 2.0 → 3.0 bump; consumers should key compatibility off the schema-version major.
Kind values: Rust is exec / proof / spec; Lean is def / theorem / abbrev / class / structure / inductive / instance / axiom / opaque / quot.
Stubs¶
An atom with code-path: "" and code-text: {lines-start: 0, lines-end: 0} is a stub — a dependency reference with no local source, i.e. an external crate or library call. Stubs are graph nodes but not code. Any count of "functions in this project" has to decide whether to include them; see Atom statuses and colours for how the UI handles the denominator.
Cross-tool operations¶
The probe CLI operates on extract output after the fact:
probe merge verus_atoms.json lean_atoms.json -o merged.json
probe enrich extract_output.json -o enriched.json
probe summary merged.json -o summary.json
| Command | What it does |
|---|---|
merge |
Combines atoms/specs/proofs from different tools into one envelope with an inputs provenance array. This is how Aeneas projects get a single graph spanning Rust and Lean. |
enrich |
Upgrades verified → transitively-verified for atoms whose entire transitive closure is verified or trusted. Implemented as reverse-BFS contamination over the dependency graph. |
summary |
Aggregates verified atoms — entrypoints, functions, lemmas. |
enrich is why two greens exist
The distinction between verified and transitively-verified is not something a probe observes directly — it is computed by enrich. probe-verus and probe-aeneas run it automatically as the last step of extract; other consumers may need to run it explicitly.
Dependencies with a missing verification-status (untracked Rust functions, spec functions) and dependencies absent from the atom map are transparent — they do not block transitive scope. Trusted dependencies are transparent too. Only an explicit unverified or failed in the closure downgrades an atom to plain verified.
This is the algorithm behind the two green strengths described in Atom statuses and colours and the statuses in the Glossary.
Validating probe output¶
The JSON Schema makes "does this output still match the contract?" a command rather than a judgement call — which matters most when upgrading a probe version.
# Structural checks only, no source needed
probe-extract-check output.json
# Full validation against the source project
probe-extract-check output.json --project /path/to/project
probe-extract-check verifies file existence, line ranges, display-name presence, kind correctness, and dependency consistency. Design notes: extract-check-design.md.
Recommended gate before rolling a probe upgrade
Probe upgrading says to "confirm extract JSON still matches SCHEMA.md before rolling production". Concretely: run the new probe image against a known repo, then validate the output with probe-extract-check and against schemas/atom-envelope.schema.json before pointing a task definition at the new tag. The atomizer's parsers accept Schema 3.0 and will fail the job otherwise.
Reference example files¶
All four probes publish an extract of the same project (curve25519-dalek), which makes them directly comparable:
| Repo | Example |
|---|---|
| probe-rust | examples/rust_curve25519-dalek_4.1.3.json |
| probe-lean | examples/lean_Curve25519Dalek_0.1.0.json |
| probe-verus | examples/verus_curve25519-dalek_4.1.3.json |
| probe-aeneas | examples/aeneas_curve25519-dalek_4.1.3.json |
Further reading in the probe repo¶
| Doc | Topic |
|---|---|
docs/schema-validation.md |
Validating output in Rust, Lean, and CI |
docs/merge-algorithm.md |
Merge algorithm specification |
docs/mappings-spec.md |
Cross-language mapping file format |
docs/envelope-rationale.md |
Why the envelope looks the way it does |
docs/ui-views.md |
How a UI should implement language toggles and graph views |
docs/categorical-framework.md |
Algebraic structure of merge |
Related¶
- Languages and plugins — how the atomizer registers and dispatches parsers
- JSON mapping — envelope → MySQL atoms
- Probe upgrading
- Atom statuses and colours
- Glossary