VeriLib for VS Code and Cursor

Formal verification progress from VeriLib, inside VS Code and Cursor.

The extension runs the real VeriLib repo browser in an editor panel. It adds a call graph view and shows each function's verification status, call graph and GitHub issues right in your source files. It drives verilib-cli to link, create, deploy and verify repos, and has a settings view for environments, API keys and colours. It works offline from your own probe output.

Features

• Repo browser: the verilib-web repo browser itself, built from source, with the Structure tree, the molecule graph and the atom drawer. It adds Open in editor and Call graph buttons, and a VeriLib web button for what the editor cannot show (the Probe Graph tab and the ← info page open there too).
• Works without a server: builds everything from your own probe output and checkout (.verilib/probes/*.json), or downloads a snapshot from verilib.org.
• Call graph: callers ← atom → callees in a layered layout, with a depth slider. Double-click an atom to drill in, use ← Back to return, and right-click for actions.
• In your code: every atom gets a CodeLens (VeriLib: <status> · Call graph · GitHub issues), the VeriLib gutter icon, a status colour and an issue highlight. Hover for details.
• GitHub issues per atom: explicit VeriLib links, plus issues whose title names exactly one function, in your code and in the repo browser's GitHub issue progress bars and drawer.
• Open in editor everywhere: each drawer accordion (Specification, Implementation, Translation) opens the atom its snippet comes from (Rust source, Lean translation, spec theorem). Blueprint statements open their source and every Lean declaration they name.
• Lite view: a lightweight browser with search, expand/collapse, one-click open, explained progress bars and atom filters: presets such as Next to verify (unfinished atoms with a verified caller) and Most called, status and call-graph chips, sorting, and your own filters saved in one global filters.json for every project.
• Chart viewer: a snapshot progress chart for probe JSON (probe-aeneas, probe-verus, probe-lean, probe-leanblueprint). By default it counts what VeriLib counts for the repo (the project's own functions with a source file), says so, and can count every entry instead.
• verilib-cli inside the editor: link or create a VeriLib repo, deploy, pull, reclone, and run its Verus structure commands from the VeriLib sidebar. See docs/cli.md.
• Probe tools: install and update probe-verus, probe-lean, probe-aeneas, probe-leanblueprint and probe-rust, get a suggestion for the open project, set its directory and flags, and run it with the stage, the time so far and the last run's duration in the notification; the output shows up in your code at once. See docs/probe.md.
• Public API: for Aeneas (Rust → Lean) projects, the crate's public API functions (is-public-api from --with-public-api) in the sidebar, with coverage, their Lean translations and specs, and the unverified callees below each one (its verification frontier). See docs/public-api.md.
• Settings view: environment (production, staging, dev, custom), an API key per environment (secret storage, shared with verilib-cli if you like), the CLI, light or dark for VeriLib's views (follows the editor by default), and a theme editor with presets and a live preview.
• Configurable per repo through .vscode/verilib.json, with a JSON schema.

Quick start

npm install
npm run compile
python3 scripts/fetch-samples.py prod:5355       # a sample: snapshot + source clone
npx @vscode/vsce package --skip-license
code --install-extension verilib-chart-viewer-*.vsix   # or: cursor --install-extension …

Then open samples/5355-curve25519-dalek-u32/src/…/field.rs and click a VeriLib: lens. Alternatively, right-click a sample's structure.json → VeriLib: Open Repo Browser.

Commands

Configuration

Settings come in three layers, and a later layer wins key by key:

1. the extension's verilib.config.json;
2. the verilibChart.config setting;
3. <repo>/.vscode/verilib.json.

VeriLib: Settings → Theme edits layers 2 and 3 visually.

{
  "status": { "verified": { "color": "#1E8E3E" }, "unspecified": { "show": false } },
  "callGraph": { "defaultDepth": 3 },
  "issues": { "matching": "linked" }
}

All keys: docs/configuration.md. Schema: verilib.config.schema.json.

How it works

The repo browser is not reimplemented. webapp/build.mjs bundles verilib-web/apps/web/src/legacy with Vite and applies seven small build-time patches; the build fails if any of them stops matching. webapp/bridge.ts routes the browser's API calls to the extension host. There, src/apiCache.ts answers from the local snapshot or a cached, GET-only proxy. The call graph (src/callGraph.ts) feeds the same renderer a layered layout of reachable atoms.

Documentation

Development

npm run compile          # TypeScript → out/
npm run build:app        # rebuild the repo browser from verilib-web (VERILIB_WEB=<path>)
npm test                 # unit tests + headless Chrome smoke tests
npm run test:vscode      # integration tests in real VS Code
npm run smoke:app        # repo browser and call graph in Chrome (Playwright)
npm run smoke:app:drag   # depth slider on a big graph
npm run smoke:lite       # Lite view
npm run smoke:drawer     # accordion and blueprint Open in editor, scrollbars
npm run smoke:settings   # the settings view
VERILIB_CLI_TEST_BIN=… npm test   # also drive a real verilib-cli against a mock server

The Playwright-based smoke tests read PLAYWRIGHT_DIR. Press F5 in this folder to run an Extension Development Host.