probe

Cross-tool atom operations for the probe-* verification tool family.

This repository contains:

• Specification documents defining the interchange format for atom files
• JSON Schema for machine-validatable envelope and atom structure
• probe CLI for cross-tool operations (currently: merge)
• probe-extract-check -- validator that checks extract JSON correctness against source code

Documentation

• docs/CONSUMER_GUIDE.md -- Start here: how to use all four probe tools, examples, and working with the data
• docs/SCHEMA.md -- Atom interchange format (Schema 2.0)
• docs/UI-VIEWS.md -- How a UI should implement language toggles, call graph / file map / crate map views
• docs/TESTING_GUIDE.md -- Testing that your visualization matches the probe data
• docs/envelope-rationale.md -- Envelope design and rationale
• docs/merge-algorithm.md -- Merge algorithm specification
• docs/translations-spec.md -- Cross-language translation file format
• docs/categorical-framework.md -- Categorical/algebraic structure of probe merge
• docs/extract-check-design.md -- Design of the extract-check validation tool
• probe-extract-check/TESTING.md -- Test guide for probe-extract-check
• schemas/atom-envelope.schema.json -- JSON Schema

Usage

# Build
cargo build

# Merge data files from different probe tools (atoms, specs, or proofs)
probe merge verus_atoms.json lean_atoms.json -o merged.json

# Run tests
cargo test

JSON Schema

The file schemas/atom-envelope.schema.json is a JSON Schema (draft 2020-12) that validates both single-tool and merged-atoms envelopes, including the core atom fields. It is the machine-readable contract that all probe-* codebases should validate against.

Validating in Rust (probe, probe-verus)

Add jsonschema as a dev-dependency and validate in tests:

use jsonschema::Validator;

#[test]
fn output_conforms_to_schema() {
    let schema: serde_json::Value =
        serde_json::from_str(include_str!("../schemas/atom-envelope.schema.json")).unwrap();
    let validator = Validator::new(&schema).unwrap();

    let output: serde_json::Value = /* your tool's JSON output */;
    assert!(validator.validate(&output).is_ok());
}

Validating in Lean (probe-lean)

Use a JSON library to parse the output and check required fields, or shell out to a schema validator:

# Using jsonschema-rs CLI (install via cargo install jsonschema-cli)
jsonschema validate --schema schemas/atom-envelope.schema.json --instance output.json

# Using Python jsonschema (pip install jsonschema)
python -m jsonschema -i output.json schemas/atom-envelope.schema.json

Validating in CI

Any CI pipeline can validate probe output against the schema. Download it from the repo:

curl -sL https://raw.githubusercontent.com/Beneficial-AI-Foundation/probe/main/schemas/atom-envelope.schema.json \
  -o atom-envelope.schema.json

What the schema covers

• Envelope structure: schema, schema-version, tool, source/inputs, timestamp, data
• Single-tool vs merged: discriminated by the schema field (probe-*/atoms vs probe/merged-*)
• Core atom fields: display-name, dependencies, code-module, code-path, code-text, kind, language
• Extensions: additionalProperties: true on atoms allows language-specific fields to pass through

Related projects

• probe-rust -- Rust call graph atoms from SCIP index
• probe-verus -- Rust/Verus call graph atoms and verification
• probe-lean -- Lean call graph atoms and verification
• probe-aeneas -- Cross-language Rust+Lean merged atoms (Aeneas projects)
• scip-callgraph -- Interactive web viewer for probe data (live demo)