Verification (--verify)

Prove that your contracts hold using formal verification with an SMT solver.

The --verify flag runs the complete verification pipeline: source checking, Viper translation, and SMT solving via Silicon/Z3. Unlike --check, which stops before Viper generation and SMT solving, --verify attempts to prove that your requires, ensures, and invariant contracts hold for all inputs under Sector9's verifier model.

Basic Usage

sector9 --verify file.sr9

On success, the command exits with code 0 after Silicon proves the obligations. On failure, it prints diagnostics describing source or proof failures and exits with a non-zero code.

What --verify Does

The verification pipeline performs these steps:

1. Source checking - All validations from --check
2. MVIR lowering - Translates Sector9 source to the MVIR intermediate representation
3. MVIR passes - Runs lowering and analysis passes including effect inference, permission scheduling, and async handling
4. Viper generation - Converts MVIR to Viper verification language
5. Silicon verification - Invokes the Viper/Silicon verifier
6. SMT solving - Z3 solver proves or disproves proof obligations
7. Diagnostics - Maps verification failures back to source locations

Verification Output

Successful verification:

✓ verification succeeded

Failed verification with diagnostics:

✗ verification failed (1 issue)

[1] Postcondition might not hold
  Assertion result == x + 1 might not hold.
  at: counter.sr9:8:4
  hint:
    - Check that the function body establishes the postcondition.

Exit Codes

Code	Meaning
0	Verification succeeded - checked contracts proven
1	Verification failed - one or more proof obligations not satisfied
2	Invalid arguments - missing files or conflicting flags
124	Timeout - verification exceeded time limit

Common Flags

Timeout Control

Set a wall-clock timeout for verification (in milliseconds):

# 30 second timeout
sector9 --verify --verify-timeout-ms 30000 file.sr9

# 2 minute timeout
sector9 --verify --verify-timeout-ms 120000 file.sr9

# No timeout; `0` disables the timeout
sector9 --verify --verify-timeout-ms 0 file.sr9

When verification times out, the process exits with code 124.

Parallelization

Run verification with multiple worker threads:

# Use 4 cores
sector9 --verify --cores 4 file.sr9

# Use 8 cores
sector9 --verify --cores 8 file.sr9

The --cores N flag maps to Silicon's parallel verifier setting as --numberOfParallelVerifiers=N-1, while keeping one coordinating thread. More cores can speed up verification of programs with multiple independent methods.

Counterexamples

Include counterexample values when verification fails:

sector9 --verify --counterexample file.sr9

When a proof fails, the counterexample shows concrete values that violate the contract:

✗ verification failed (1 issue)

[1] Postcondition might not hold
  Assertion result > 0 might not hold.
  at: example.sr9:5:4
  counterexample:
    x = 0

JSON Output

Emit structured JSON diagnostics:

sector9 --verify --json file.sr9

This outputs machine-readable JSON with schema version 2, useful for IDE integration and CI pipelines. The JSON includes source locations, snippets, hints, and optional counterexamples. See JSON Output.

Intermediate Viper Output

Save the generated Viper program for debugging:

sector9 --verify --verify-vpr-out output.vpr file.sr9

The .vpr file shows how Sector9 encodes your Sector9 program for verification. This is useful for understanding verification failures at the Viper level, especially alongside --viper.

Debugging Flags

# Log Viper/Silicon invocation details
sector9 --verify --viper-verbose file.sr9

# Echo Silicon stdout/stderr even on success
sector9 --verify --viper-trace file.sr9

# Keep generated Viper files on success
sector9 --verify --viper-keep-vpr file.sr9

Integer Mode

Verified code requires checked fixed-width integer semantics:

# Checked mode (default) - prove no overflow/underflow
sector9 --verify --int-mode checked file.sr9

--verify --int-mode unchecked and --verify --int-mode bitvec are rejected. See Integer Mode.

Deterministic Artifacts

Enable deterministic Viper output for reproducible builds:

sector9 --verify --deterministic file.sr9

--verify vs --check

Aspect	--check	--verify
Source/type checking	Yes	Yes
Contract parsing	Yes	Yes
Viper generation	No	Yes
SMT solving	No	Yes
Proof verification	No	Yes
Speed	Fast (seconds)	Slower (depends on complexity)
Use case	Development iteration	Pre-deployment validation

Use --check for rapid iteration during development. Use --verify when you need mathematical proof that contracts hold.

Environment Variables

Variable	Effect
XDG_CACHE_HOME	Override cache directory for Viper files
VIPER_SERVER	Path to custom viperserver.jar
SILICON_FLAGS	Additional flags passed to Silicon
SECTOR9C_VERIFY_KEEP_VPR	Keep Viper files on success (non-empty = true)

Verification Outcomes

Tests and source files use naming conventions to indicate expected outcomes:

Suffix	Meaning
_sat	Verification should succeed
_unsat	Verification should fail (expected counterexample)
_reject	Type checking should fail before verification

For example:

• counter_sat.sr9 - contracts should be proven
• counter_unsat.sr9 - contains a deliberate bug, verification should fail
• counter_reject.sr9 - has a type error, rejected before verification

Typical Workflow

# 1. Fast iteration with type checking
sector9 --package core ./core/src --check my_actor.sr9

# 2. Fix any type or contract syntax errors

# 3. Run verification when --check passes
sector9 --package core ./core/src --verify my_actor.sr9

# 4. If verification fails, analyze the failure
sector9 --package core ./core/src --verify --counterexample my_actor.sr9

# 5. Debug complex failures with Viper output
sector9 --package core ./core/src --verify --verify-vpr-out debug.vpr my_actor.sr9

# 6. On verification success, proceed to deployment

CI/CD Integration

For continuous integration, combine timeout and JSON output:

# CI-friendly verification with timeout and machine-readable output
sector9 --verify --json --verify-timeout-ms 300000 my_actor.sr9

Parse the JSON output to integrate with test reporters. The exit code indicates overall success or failure.

Performance Tips

1. Start with --check - Catch type errors before expensive verification
2. Use --cores - Parallelize verification for programs with multiple methods
3. Set timeouts - Prevent runaway verification in CI
4. Minimize quantifiers - Complex forall/exists can slow verification
5. Use triggers - Guide the SMT solver with forallWith triggers
6. Modularize - Verify smaller modules independently
7. Run --check first - It catches frontend and shared-boundary errors before Silicon starts

Troubleshooting

Verification times out

• Increase --verify-timeout-ms for legitimate long proofs, or reduce it in CI to fail fast on regressions
• Use --counterexample on failures where Silicon returns a model
• Simplify quantifiers or add explicit triggers
• Break large methods into smaller helpers

"Insufficient permission" errors

• Add missing reads or modifies clauses
• Check that all accessed fields are declared in footprints

Postcondition might not hold

• Use --counterexample to see failing values
• Add intermediate assert statements to isolate the issue
• Strengthen preconditions to rule out impossible inputs

Verification succeeds but takes too long

• Use --cores for parallelization
• Profile with --viper-trace to identify slow methods
• Consider using trusted for expensive methods during development

Summary

• --verify proves contracts hold using SMT solving
• Use --counterexample to debug failing verifications
• Use --verify-timeout-ms and --cores for performance control
• Use --json for CI/CD integration
• Combine with --check for efficient development workflow