Understanding Verification Output

Reading verification results: what "verified" means, what failures look like, and how to interpret the different output types.

The Two Outcomes

When you run sector9 --verify, the verifier reports one of two outcomes:

Success

✓ verification succeeded

This means the verifier proved that all checked obligations hold for inputs allowed by the specification, under Sector9's verifier model and trusted assumptions. The program is correct with respect to those specifications.

Exit code: 0

Failure

✗ verification failed (1 issue)

------------------------------
[1] Postcondition of add might not hold
  Postcondition of add might not hold. Assertion $Res == a + b + 1 might not hold.
  method: add
  at: sector9-....vpr:185:19
  hint:
    - Strengthen the implementation or weaken the ensures.

This means at least one obligation could not be proven. The program may have a bug, the specification may be too strong, or an extra precondition/invariant may be needed.

Exit code: 1

Exit Codes

Code	Meaning
0	Verification succeeded
1	Verification failed or type checking failed
2	Invalid command-line arguments or missing files
124	Verification timed out

Error Categories

Sector9 reports two categories of errors:

1. Type and Translation Errors

These occur before verification, during type checking or translation to the verification backend.

example.sr9:5.10-5.15: type error [M0314], ghost variable g cannot be used in runtime code

Format: file:line.col-line.col: error type [code], description

Common type errors:

• M0031 - Shared function has non-shared parameter type
• M0072 - Field does not exist in type
• M0314 - Ghost variable used in runtime code

Translation errors:

example.sr9:18.7-18.48: viper error [0], translation to viper failed: loop invariant contains allocation

These indicate unsupported constructs or semantic violations in the verification translation.

2. Verification Failures

These occur when the SMT solver finds an obligation that cannot be proven.

[1] Postcondition of increment might not hold
  Postcondition of increment might not hold.
  method: increment
  at: counter.sr9:11:4
  snippet:
      ensures result == count;
  hint:
    - Strengthen the implementation or weaken the ensures.

Obligation Types

Each verification failure identifies the type of contract that failed:

Obligation	Meaning
Precondition	A requires clause was not satisfied at a call site
Postcondition	An ensures clause could not be proven
Assert	An assert statement could not be proven
Loop invariant	A loop invariant was not maintained
Invariant	An actor invariant was not preserved

Reading Failure Details

Each failure includes:

1. Index - [1], [2], etc. for multiple failures
2. Obligation type - What kind of contract failed
3. Message - Description of the issue
4. Method - Which function contains the failure
5. Location - File, line, and column. This is usually a source span, but may be a generated Viper span when source mapping is unavailable.
6. Snippet - The relevant source code
7. Hint - Suggested fixes

Output Formats

Sector9 supports three output formats:

Human-Readable (Default)

Best for interactive use. Shows colors in the terminal:

sector9 --verify counter.sr9

JSON

Machine-readable structured output:

sector9 --verify --json counter.sr9

Returns a structured object with schema_version, status, failures, warnings, and backend details. Use this for CI/CD integration or when parsing output programmatically.

TOON

Compact format designed for LLM-friendly parsing:

sector9 --verify --toon counter.sr9

Uses a key-value format with minimal syntax overhead.

Getting Counterexamples

Add --counterexample to ask for concrete values that cause a failure:

sector9 --verify --counterexample counter.sr9

Output includes:

Counterexample summary
  - return: a=0, b=0, $Res=0

When a model is available, this shows variable values at the point of failure and helps you understand why the contract does not hold. Counterexamples prefer source names when available, but generated names such as $Res can appear.

Debugging Workflow

When verification fails:

1. Read the obligation type - Is it a postcondition, precondition, or assertion?
2. Check the location - Which line of code is the issue?
3. Review the snippet - What does the contract claim?
4. Add --counterexample - Get concrete values that violate the contract
5. Trace the logic - Follow the code path with those values

Example

Given this failure:

[1] Postcondition of increment might not hold
  Postcondition of increment might not hold.
  method: increment
  at: counter.sr9:11:4

Ask yourself:

• What does result contain when the function returns?
• What does count contain at that moment?
• Are they equal in all cases?

Quick Reference

Command	Purpose
sector9 --check file.sr9	Source check without SMT solving
sector9 --verify file.sr9	Full verification
sector9 --verify --counterexample file.sr9	Verification with failing values
sector9 --verify --json file.sr9	JSON output for tooling

Summary

• ✓ verification succeeded means checked obligations were proven for all inputs allowed by their preconditions
• ✗ verification failed shows which obligations could not be proven
• Exit code 0 means success, 1 means failure
• Type errors occur before verification, verification failures occur during
• Use --counterexample to see concrete failing values
• Use --json for machine-readable output in CI/CD