Skip to content

Verification in CI

Two independent ways to keep verification honest on every pull request:

You want to… Use
Track sorrys and spec changes in a Lean 4 project, with a PR comment veritooling — reusable GitHub Actions
Keep a VeriLib repository's .verilib/ structure in sync and gate on proof status verilib-cli --check-only

They solve different problems and compose: veritooling reports what changed in your proofs; the CLI enforces that your structure files still match your code.

veritooling (Lean 4)

veritooling is a reusable CI toolkit — you reference its workflows from your own repo rather than copying scripts. It builds a Lean project, audits which declarations are sorry-tainted, diffs that against the base branch, and posts a sticky Verification Delta comment.

lake build  ──▶  audit (manifest + report)  ──▶  delta vs base  ──▶  PR comment
            (lean-build-audit.yml)                 (verification-comment.yml)

Why two workflows

The build and the comment run as separate jobs by design. The build runs untrusted PR code with no write access; the comment job — which needs pull-requests: write — only ever sees the artifacts the build produced. That is what lets fork PRs get comments without exposing a write token to untrusted code.

Setup

Two files in your repository.

.github/workflows/lean-ci.yml — build and audit:

name: Lean CI
on:
  pull_request:
  push:
    branches: [main]

jobs:
  build:
    uses: Beneficial-AI-Foundation/veritooling/.github/workflows/lean-build-audit.yml@v1
    with:
      sorry-backend: probe        # zero-config

.github/workflows/verification-comment.yml — post the comment:

name: Verification Comment
on:
  workflow_run:
    workflows: ["Lean CI"]
    types: [completed]

jobs:
  comment:
    uses: Beneficial-AI-Foundation/veritooling/.github/workflows/verification-comment.yml@v1

Choosing a backend

Backend How it detects sorry When to use
probe Parses build warnings via probe-lean. Zero config; auto-detects the root module. Default. Start here.
collectaxioms A Lean metaprogram that walks the transitive axiom closure of each declaration. Catches sorry reached indirectly, plus Lean.trustCompiler and custom axioms. When indirect taint matters — i.e. when a theorem looks clean but depends on something that isn't. 
    with:
      sorry-backend: collectaxioms
      root-module: MyProject      # optional; auto-detected from lakefile.toml defaultTargets
      exclude-module: Extracted   # optional; keeps generated code out of the detailed view

Reading the collectAxioms report

It logs four sections, and two of them count different things — this trips people up:

Section Scope Counts
1. Axiom & sorry audit Audited modules only (exclude-module narrows this) Theorems and axioms — your claims
2. Where does sorry come from? Same BFS chain from a tainted theorem down to the declaration containing the sorry
3. Full project summary Every module All declaration kinds, including definitions
4. Sorry manifest Every module All sorry-tainted declarations — the machine-readable file feeding the delta

So the manifest count is usually higher than section 2's, because it includes unfinished definitions, not just tainted theorems. That is expected, not a bug.

Reducing comment noise

On projects carrying sorrys in generated or extracted code, gate the comment on hand-written modules so it only fires for a genuinely new hand-written sorry:

jobs:
  comment:
    uses: Beneficial-AI-Foundation/veritooling/.github/workflows/verification-comment.yml@v1
    with:
      include-prefix: MyProject

The underlying actions

The workflows compose self-contained composite actions you can also use individually — useful when the audit needs to share a job with other steps (for example a docs-site build on the same lake build):

Action Phase Purpose
sorry-audit-collectaxioms Generation Transitive axiom-closure detection
sorry-audit-probe Generation Detection via probe-lean
specs-delta Generation Detect specification-theorem changes
sorry-delta Reporting Diff manifests, format the delta
verification-delta-report Reporting Combine deltas into one PR comment

Long-run progress

tools/verification-progress-history is a standalone CLI (not an Action) that reconstructs a project's verification progress across git history — weekly samples of tracked / verified / translated — into a JSONL + CSV burn-up series. Use it for reporting rather than per-PR gating.

verilib-cli --check-only

For repositories connected to the VeriLib platform, the CLI's check-only mode fails CI without rewriting files:

verilib-cli atomize --check-only
verilib-cli specify --check-only
verilib-cli verify  --check-only
Command Fails when
atomize --check-only Stubs do not match the enriched stubs.json
specify --check-only A stub with specs is missing a certificate
verify --check-only Any stub has status failure

Set "auto-validate-specs": true in .verilib/config.json so specs are certified without an interactive prompt.

When probe output is generated elsewhere (a job queue, a Docker step, or the server-side atomizer), add --no-probe so the CLI validates against pre-generated JSON instead of invoking a probe itself:

verilib-cli atomize --no-probe --check-only
verilib-cli specify --no-probe --check-only
verilib-cli verify  --no-probe --check-only

Full details: CLI workflows.

Validating probe output in CI

If your pipeline produces probe JSON, validate it against the published JSON Schema rather than eyeballing it:

probe-extract-check output.json --project .

See Probe ecosystem.