probegraph
Dependency and call graph generation, complexity metrics, and interactive
visualization for verified codebases. Graphs come from multiple probes:
- probe-lean — Lean 4 declarations (atom JSON), with
sorry detection
- probe-verus / probe-rust — Rust and Verus projects via SCIP indices
- probe-aeneas — cross-language Rust↔Lean mapping links, merged graphs
The web viewer's primary input is probe atom JSON (probe-lean, probe-verus);
SCIP is one probe among several. This workspace also computes Halstead
complexity metrics for Verus specifications and proofs.
Live demo: https://beneficial-ai-foundation.github.io/probegraph/
Workspace structure
probegraph/
├── crates/
│ ├── scip-core/ # SCIP parsing, call graph construction, D3 export
│ ├── verus-metrics/ # Halstead metrics for Verus specs/proofs
│ └── metrics-cli/ # Command-line tools (37 binaries, including pipeline)
├── external/
│ └── verus_lemma_finder/ # Similar lemma search (git submodule)
├── web/ # Interactive viewer (see web/README.md)
├── scripts/ # Python enrichment and plotting scripts
├── examples/ # detect_unused_specs example script
└── docs/
├── guides/ # Using probegraph: CI, viewer, metrics
├── technical/ # Internals: scip-core, spec/proof metrics, CLI tools
├── plans/ # Work in progress
└── archive/ # Historical design docs and analyses
Quick start: graph your own project
The pipeline binary produces an enriched graph in one step (Rust/Verus
projects):
git clone --recurse-submodules https://github.com/Beneficial-AI-Foundation/probegraph.git
cd probegraph
cargo build --release --workspace
# Optional, for the similar-lemmas feature:
uv sync --extra enrich
(cd external/verus_lemma_finder && uv tool run maturin develop --release)
cargo run --release --bin pipeline -- /path/to/verus-project
cd web && npm install && npm run dev
The pipeline generates a SCIP index, exports the call graph to
web/public/graph.json (change with -o), runs verification to attach
statuses, and adds similar lemmas. Useful flags:
| Flag | Effect |
|---|
--skip-verification | Faster; no Verus needed |
--skip-similar-lemmas | No Python needed |
--use-cached-scip | Reuse <project>/index.scip.json if it exists |
--github-url <url> | Source links in the viewer |
-p <crate> | Select a package in a workspace |
--use-rust-analyzer | Plain Rust projects (combine with --skip-verification) |
The viewer guide covers the views, filters and
queries.
Generating a SCIP index manually
Install rust-analyzer
(or verus-analyzer) and
scip, then, in the project directory:
rust-analyzer scip .
scip print --json index.scip > index.scip.json
CI integration
Reusable workflows build the graph in your repo's CI and deploy the viewer to
GitHub Pages. Minimal setup for a Verus project:
permissions:
contents: read
pages: write
id-token: write
jobs:
callgraph:
uses: Beneficial-AI-Foundation/probegraph/.github/workflows/generate-callgraph.yml@main
Lean 4 projects use generate-lean-callgraph.yml the same way. Inputs, plain
Rust projects and subpath deployment are covered in the
CI integration guide.
Verus metrics
Computes Halstead metrics for requires/ensures/decreases clauses and
proof { } blocks (with transitive lemma analysis), and merges
implementation-complexity metrics from rust-code-analysis:
cargo run -p metrics-cli --bin run_full_pipeline -- \
--scip index.scip.json --csv functions_to_track.csv \
--rca-dir rca_jsons/ --proof-csv proofs.csv --output-dir out/
See the metrics pipeline guide for the
inputs and steps.
Documentation
License
MIT; see LICENSE.
