Human-Readable Output

Default colored terminal output for interactive use.

Human-readable output is the default format when running Sector9 commands. It uses colors and structured formatting to make verification results easy to read in a terminal. This format is optimized for developers debugging verification failures interactively.

When to Use

Use human-readable output (the default) when:

• Running verification interactively in a terminal
• Debugging verification failures manually
• Learning how Sector9 verification works

Use other formats for:

• --json - CI/CD pipelines, IDE integration, programmatic processing
• --toon - LLM-assisted debugging, AI tools

Structured formats are primarily for --verify. Plain --check frontend diagnostics remain line-oriented unless you run through --verify --json or --verify --toon and the error is reported before Silicon starts.

Success Output

When verification succeeds, the output is minimal:

✓ verification succeeded

The checkmark (✓) appears in bold when colors are enabled. The command exits with code 0.

Failure Output

When verification fails, the output includes structured diagnostics:

✗ verification failed (2 issues)

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

------------------------------
[2] Precondition might not hold
  Precondition n > 0 might not hold at this call site.
  method: divide
  at: math.sr9:15:12
  snippet:
      divide(x)
  hint:
    - Add a precondition to the caller that implies the callee's precondition.
    - Add a guard to ensure n > 0 before calling.

The command exits with code 1.

Output Structure

Each verification failure contains these fields:

Field	Description
Index	[1], [2], etc. - Sequential failure number
Obligation	Type of proof obligation that failed
Message	What the verifier could not prove
method:	Function or method where failure occurred
label:	Named assertion label (if present)
at:	Source location as file:line:column
snippet:	Relevant source code excerpt
hint:	Suggestions for fixing the failure

Not all fields appear for every failure. For example, label: only appears when the failing assertion has a named label.

Obligation Types

Common obligation types in failure messages:

Obligation	Meaning
Postcondition	ensures clause could not be proven
Precondition	requires clause not satisfied at call site
Assert	assert statement could not be proven
Invariant	Actor or loop invariant not maintained
Permission	Missing reads or modifies for field access
Framing	Field changed that wasn't in modifies clause

Color Scheme

When output goes to a terminal (TTY), colors are automatically enabled:

Element	Color
Success header (✓)	Bold
Failure header (✗)	Bold red
Warning header	Bold yellow
Field labels (method:, at:, etc.)	Cyan
Separator lines	Cyan
Hints	Yellow

Colors are automatically disabled when output is redirected to a file or pipe. This happens automatically based on TTY detection.

Warnings

Warnings appear before failure details:

Warnings
  - M0145: pattern does not cover value false
  - M0237: The compare argument can be inferred and omitted here.

✗ verification failed (1 issue)
...

Warnings do not cause verification to fail. Use -Werror to treat warnings as errors.

Counterexamples

When using --counterexample, failing values appear after the failure details:

✗ verification failed (1 issue)

------------------------------
[1] Postcondition might not hold
  Assertion result > 0 might not hold.
  at: example.sr9:5:4
  snippet:
      ensures result > 0;

Counterexample summary
  - return: x=-5, result=0

The counterexample shows concrete values that violate the contract, helping identify why verification failed.

Type Checking Errors

Type errors from --check use a different format:

counter.sr9:5:12: type error [M0026], unbound variable x

Format: file:line:column: category severity [code], message

Type errors include:

• Location - Precise source position
• Category - type, import, syntax, etc.
• Severity - error, warning, or info
• Code - Error code like M0026 for reference
• Message - Human-readable explanation

Use sector9 --explain M0026 to request a detailed explanation when one exists for that code. Use --json or --toon when a verification pipeline needs structured output.

Comparing Formats

Aspect	Human	JSON	TOON
Target audience	Developers	Tools	LLMs
Colors	Yes (TTY)	No	No
Structured data	No	Yes	Yes
Easy to parse	No	Yes	Yes
Default	Yes	No	No
Flag needed	None	--json	--toon

Disabling Colors

Colors are automatically disabled when:

• Output is piped to another command
• Output is redirected to a file
• The terminal is not a TTY

There is no explicit flag to disable colors. If you need uncolored output in a TTY context, redirect through cat:

sector9 --verify file.sr9 | cat

Examples

Simple Verification Success

$ sector9 --verify counter.sr9
✓ verification succeeded

Verification Failure with Hints

$ sector9 --verify buggy.sr9
✗ verification failed (1 issue)

------------------------------
[1] Postcondition might not hold
  Assertion result >= 0 might not hold.
  method: withdraw
  at: buggy.sr9:12:4
  snippet:
      ensures result >= 0;
  hint:
    - The postcondition requires a non-negative result.
    - Check that withdraw cannot return negative values.

Multiple Failures

$ sector9 --verify complex.sr9
✗ verification failed (3 issues)

------------------------------
[1] Precondition might not hold
  ...

------------------------------
[2] Invariant might not hold
  ...

------------------------------
[3] Assert might not hold
  ...

Type Error Output

$ sector9 --check typo.sr9
typo.sr9:7:14: type error [M0026], unbound variable balanse

Summary

• Human-readable output is the default format
• Colors are auto-enabled for TTY, disabled for pipes/files
• Verification failures show obligation type, location, snippet, and hints
• Type errors show location, error code, and message
• Use --json for tooling integration, --toon for LLM tools
• Use --counterexample to see concrete failing values
• If verification cannot find viperserver.jar, the command exits before producing structured proof diagnostics; set VIPER_SERVER or rebuild the toolchain.