TOON Format (--toon)

LLM-friendly output format for AI-assisted debugging.

TOON (Text-Oriented Object Notation) provides structured verification diagnostics in a compact, human-readable format optimized for consumption by large language models. It is derived from JSON output, but drops redundant fields and adds a few derived convenience fields such as primary_span, failure_stage, and error_code to keep context small for AI agents.

When to Use

Use TOON output (--toon) when:

• Feeding verification results to AI assistants or LLM-based tools
• Building automated debugging pipelines with AI integration
• Working with agents that analyze and fix verification failures
• Preferring structured output that remains human-readable

Use other formats for:

• Human-readable (default) - Interactive terminal debugging with colors
• --json - CI/CD pipelines, IDEs, and traditional tooling

Basic Usage

Enable TOON output with the --toon flag:

sector9 --package core ./core/src --verify --toon file.sr9

The TOON output is printed to stdout. Redirect to a file for processing:

sector9 --package core ./core/src --verify --toon file.sr9 > results.toon

Success Output

When verification succeeds:

schema_version: "2"
status: VALID
failures[0]:
warnings[0]:

The status field is VALID and the command exits with code 0. Backend setup failures, such as a missing viperserver.jar, occur before structured TOON verifier output is available.

Failure Output

When verification fails, the output includes detailed failure entries:

schema_version: "2"
status: INVALID
failures[1]:
  - failure_id: d017ca6529e6b16a1b529fbc00c46f8c
    failure_kind: verification
    failure_stage: verification
    error_code: verification.postcondition
    obligation_kind: postcondition
    msg: "Postcondition of increment might not hold."
    obligation: Postcondition might not hold
    method: increment
    label: null
    motoko_span:
      file: counter.sr9
      line: 8
      col: 4
      endLine: 8
      endCol: 28
    viper_span:
      file: counter.vpr
      line: 146
      col: 19
      endLine: 146
      endCol: 35
    motoko_snippet: "    ensures result == x + 1;"
    primary_span:
      file: counter.sr9
      line: 8
      col: 4
      endLine: 8
      endCol: 28
    primary_snippet: "    ensures result == x + 1;"
    span_origin: sector9
    fix_hints[1]: Strengthen the implementation or weaken the ensures.
warnings[0]:

The status field is INVALID and the command exits with code 1.

TOON Format Rules

TOON uses several formatting conventions to remain compact and readable:

Key-Value Pairs

Simple values appear on the same line:

status: VALID
line: 42
method: increment

Nested Objects

Objects are indented with 2 spaces per level:

motoko_span:
  file: counter.sr9
  line: 8
  col: 4

Primitive Arrays

Arrays of primitives (strings, numbers, booleans) are inlined:

fix_hints[2]: Add precondition,Strengthen invariant

Object Arrays

Arrays of objects use list format with - prefix:

failures[2]:
  - failure_id: abc123
    method: foo
  - failure_id: def456
    method: bar

Tabular Arrays

Arrays of objects with identical keys use a compact table format:

bindings[3]{name,value,kind}:
  x,0,local
  y,5,local
  result,5,internal

Empty Arrays

Empty arrays show their zero length:

failures[0]:
warnings[0]:

Quoting Rules

TOON quotes strings only when necessary:

• Empty strings: ""
• Contains :, ,, spaces, newlines, tabs: "value with spaces"
• Reserved words: "true", "false", "null"
• Starts with -, [, or {: "-prefix"
• Numeric strings: "123"

Escape sequences in quoted strings:

• \n for newline
• \t for tab
• \r for carriage return
• \\ for backslash
• \" for double quote

Counterexamples

Use --counterexample (or --models) to include concrete failing values:

sector9 --package core ./core/src --verify --toon --counterexample file.sr9

The counterexample appears in the failure:

failures[1]:
  - failure_id: abc123
    obligation_kind: postcondition
    method: withdraw
    counterexample:
      models[1]:
        - label: return
          bindings[3]{name,value,kind,scope}:
            amount,100,local,local
            balance,50,field,field
            result,50,internal,internal

The tabular format makes it easy to scan multiple bindings at once.

Schema Structure

TOON is a compact view derived from JSON output (version 2). It keeps core fields, omits redundant ones, and may add derived fields such as primary_span, failure_stage, error_code, and counterexample_brief.

Top-level fields:

Field	Description
schema_version	Always 2 for current Sector9 versions
status	VALID, INVALID, or ERROR
failures	List of verification failure objects
warnings	List of warning objects
backend_error	Backend error summary (present when verification fails without structured failures)
silicon	Raw verifier backend output (only with --viper-verbose or --viper-trace)

See JSON Output for complete schema documentation.

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
Schema versioned	No	Yes	Yes
Compact	No	No	Yes
Default	Yes	No	No
Flag needed	None	--json	--toon

Flag Interactions

The --toon flag interacts with other flags:

Flag	Effect
--json	Mutually exclusive - last one wins
--counterexample	Adds counterexample models (does not change format)
--models	Alias for --counterexample
--verify-timeout-ms	Works with TOON; timeout status reflected in output
--hide-warnings	Suppresses warning output
--viper-verbose	Keeps raw backend output (silicon) in TOON
--viper-trace	Keeps raw backend output and prints additional backend traces

Counterexample output has the same backend requirement as --json --counterexample; see Counterexamples.

AI-Assisted Debugging Workflow

TOON is designed for iterative debugging with AI assistance:

1. Run verification with TOON output:

   sector9 --package core ./core/src --verify --toon --counterexample buggy.sr9 > diag.toon

2. Feed output to an LLM with your source code

3. The LLM can parse:

   • Which obligations failed (obligation_kind)
   • Where failures occurred (motoko_span)
   • Concrete failing values (bindings)
   • Suggested fixes (fix_hints)

4. Apply LLM-suggested fixes and repeat

The compact format preserves context window space while providing all necessary debugging information.

Examples

Successful Verification

$ sector9 --package core ./core/src --verify --toon counter.sr9
schema_version: "2"
status: VALID
failures[0]:
warnings[0]:

Failed Postcondition with Counterexample

$ sector9 --package core ./core/src --verify --toon --counterexample arith.sr9
schema_version: "2"
status: INVALID
failures[1]:
  - failure_id: 7f3c2a1b
    failure_stage: verification
    error_code: verification.postcondition
    obligation_kind: postcondition
    msg: "Postcondition of add might not hold."
    method: add
    motoko_span:
      file: arith.sr9
      line: 5
      col: 4
    primary_span:
      file: arith.sr9
      line: 5
      col: 4
    fix_hints[1]: Strengthen the implementation or weaken the ensures.
    counterexample_brief:
      models[1]:
        - label: return
          bindings[3]{name,value}:
            a,0
            b,0
            result,0

Multiple Failures

$ sector9 --package core ./core/src --verify --toon multi_error.sr9
schema_version: "2"
status: INVALID
failures[2]:
  - obligation_kind: postcondition
    method: foo
    msg: "Postcondition of foo might not hold."
  - obligation_kind: precondition
    method: bar
    msg: "Precondition of bar might not hold."

Parsing TOON Output

TOON is designed for LLM consumption, but you can also parse it programmatically. Key patterns:

• Look for status: VALID or status: INVALID
• Count failures with failures[N]: where N > 0 indicates failures
• Extract method names after method:
• Find source locations under motoko_span:
• Read fix suggestions after fix_hints[N]:

For traditional tooling, consider using --json instead, which is easier to parse with standard JSON libraries.

Summary

• Use --toon to enable LLM-friendly structured output
• TOON is derived from JSON and omits redundant fields; use --json for full fidelity
• Tabular arrays and inline primitives reduce token usage
• Add --counterexample to include concrete failing values
• Exit codes match verification status (0 = valid, 1 = invalid)
• Ideal for AI-assisted debugging workflows