Project Settings

Backbuild Prove settings control how verification behaves for your project: how failures are reported, which files are skipped, how long a proof may run, and how much parallelism to use.

After this page you will be able to choose a severity mode for development versus CI, exclude paths you do not want verified, tune timeouts and parallelism, and understand how settings are resolved.

Settings File

Project settings are stored in .backbuild-cli/prove.json at the project root. This file is written the first time you change a setting with backbuild prove settings (for example --severity-mode strict). Until then, verification runs with the built-in defaults shown below.

{
  "severity_mode": "strict",
  "exclude_patterns": [],
  "timeout_ms": 60000,
  "max_parallel": 4
}

The settings file should be committed to version control so that all team members and CI pipelines use the same configuration.

severity_mode

Controls how proof failures are reported. This affects both the CLI exit code and the VS Code extension’s diagnostic severity.

Mode	CLI Behavior	IDE Behavior	Use Case
strict	Exit code 1 on any failure. CI pipeline fails.	Failed proofs shown as errors (red squiggles).	CI pipelines, production branches, safety-critical code.
warn	Exit code 0 even with failures. Failures printed as warnings.	Failed proofs shown as warnings (yellow squiggles).	Active development, onboarding to formal verification.
lenient	Exit code 0. Failures printed as informational notes.	Failed proofs shown as information (blue squiggles).	Exploratory work, learning the system, large legacy codebases.

Setting via CLI

backbuild prove settings --severity-mode strict

Setting via VS Code

In VS Code Settings, search for backbuild.severityMode and select the desired diagnostic severity (warning or error) from the dropdown.

Recommended Workflow

A common pattern is to use warn mode during development and strict mode in CI:

# In .backbuild-cli/prove.json (committed to repo)
{
  "severity_mode": "warn"
}

# In CI pipeline (overrides project setting)
backbuild prove ci --format json
# CI exits 1 on failures regardless of severity_mode

Note: backbuild prove ci always uses exit codes to signal failures, regardless of the severity_mode setting. The severity mode only affects interactive output formatting and IDE diagnostic severity.

exclude_patterns

An array of glob patterns specifying files and directories to skip during verification. Annotations in excluded files receive a Skipped status.

{
  "exclude_patterns": [
    "tests/fixtures/**",
    "vendor/**",
    "generated/**",
    "**/*.test.ts",
    "**/*.spec.rs"
  ]
}

Managing via CLI

# Add an exclusion pattern
backbuild prove settings --add-exclude "tests/fixtures/**"

# Remove an exclusion pattern
backbuild prove settings --remove-exclude "tests/fixtures/**"

Common Exclusions

Pattern	Purpose
vendor/**	Skip vendored dependencies
node_modules/**	Skip Node.js dependencies
tests/fixtures/**	Skip test fixture files
generated/**	Skip auto-generated code
**/*.test.*	Skip test files
**/*.spec.*	Skip spec files
migrations/**	Skip database migration files

timeout_ms

The maximum time in milliseconds allowed for verifying a single pf2 annotation. If the kernel does not return a result within this time, the annotation is reported as a timeout failure.

Setting	Default	Range
timeout_ms	60000 (60 seconds)	1000 to 600000 (1 second to 10 minutes)

Most annotations verify in under a second. Complex proofs with many steps or deep theorem chains may take longer. Increase the timeout if you have proofs that consistently time out.

# Set a 2-minute timeout
backbuild prove settings --timeout 120000

max_parallel

The maximum number of annotations to verify concurrently. Higher values speed up verification for projects with many annotations, but use more server resources.

Setting	Default	Range
max_parallel	4	1 to 16

# Run up to 8 verifications in parallel
backbuild prove settings --max-parallel 8

For CI pipelines running on machines with many cores, increasing max_parallel can significantly reduce total verification time.

Full Example

A typical .backbuild-cli/prove.json for a production project:

{
  "severity_mode": "strict",
  "exclude_patterns": [
    "vendor/**",
    "node_modules/**",
    "tests/fixtures/**",
    "generated/**"
  ],
  "timeout_ms": 60000,
  "max_parallel": 4
}

Precedence

Settings are resolved in this order (highest priority first):

1. CLI flags: command-line options override all other settings for that invocation.
2. Project settings: .backbuild-cli/prove.json in the project root.
3. Defaults: built-in default values.

The VS Code extension keeps its own diagnostic-severity setting (backbuild.severityMode, with values warning or error) in your VS Code configuration. It controls how the IDE renders failing proofs and is separate from the CLI’s .backbuild-cli/prove.json, which the backbuild prove CLI reads.

Next Steps

• CLI and CI: all CLI commands and options
• Editor Extensions: editor-specific configuration
• Getting Started: install and run your first verification