Incremental Proofs

ImandraX's architecture is designed for large-scale verification projects with many definitions and theorems. Its incremental and parallel proof system dramatically reduces re-verification time as you iterate on your code.

Key features

Incremental checking

ImandraX tracks dependencies between definitions, theorems, and lemmas. When you modify a file, only the items whose dependencies have changed are re-verified:

• Change a function definition → re-verify theorems that mention it
• Change a lemma → re-verify theorems that use it as a rewrite rule
• Add a new theorem → verify only the new theorem (nothing else changes)

Unchanged items are cached and not re-checked. This means that in a file with 100 theorems, editing one function might trigger re-verification of only 3 theorems.

Parallel proof execution

Independent proofs run concurrently across multiple CPU cores. ImandraX analyzes the dependency graph and schedules non-dependent proofs in parallel:

• If theorems A and B have no shared dependencies, they're verified simultaneously
• If theorem C depends on lemma L, C waits for L to complete (or uses prior-lemma assumptions)
• CPU utilization scales with the number of independent proof obligations

Prior-lemma assumptions

A distinctive feature of ImandraX: you can start using a lemma before its proof is complete. ImandraX proceeds under the assumption that the lemma will be proved, allowing dependent work to continue in parallel.

If the lemma's proof later fails, all work that depended on it is invalidated and re-checked. But in the common case (the lemma succeeds), this saves significant time by avoiding sequential bottlenecks.

Impact on workflow

In VS Code

The VS Code extension takes full advantage of incremental checking:

• As you type, only affected proofs are re-verified
• Green/red indicators update incrementally — previously proved theorems stay green
• The goal state viewer reflects the latest proof state without re-verifying the entire file
• You get fast feedback even in files with hundreds of definitions

In CI/CD

Use imandrax-cli check in your build pipeline. The CLI leverages caching:

# First run: verifies everything
imandrax-cli check myproject.iml
 
# Subsequent runs: only re-verifies changed dependencies
imandrax-cli check myproject.iml

In multi-file projects

Import dependencies ([@@@import]) are tracked. When you save a utility file, only files that import it are re-checked, and within those files, only affected definitions.

How it works

ImandraX maintains a dependency graph of all definitions and proofs:

1. Definitions depend on the types and functions they reference
2. Theorems depend on the definitions they mention and the rules they use
3. Files depend on the files they import

When a node in the graph changes, ImandraX:

1. Marks all downstream dependents as "stale"
2. Re-verifies stale items in topological order
3. Runs independent items in parallel
4. Caches results for future use

This is a key architectural advancement over Imandra Core, which processed definitions and proofs sequentially.

Comparison with Imandra Core