JSON Output (--json)

Machine-readable structured diagnostics for tooling integration.

JSON output provides a structured format for verification results, designed for CI/CD pipelines, IDE integrations, and programmatic processing. The output follows a versioned schema (currently version 2) that includes detailed source locations, code snippets, fix hints, and optional counterexamples. Use it with --verify; plain --check --json is not the structured diagnostics path.

When to Use

Use JSON output (--json) when:

• Building CI/CD pipelines that parse verification results
• Integrating Sector9 with IDEs or editors
• Writing tools that process verification failures programmatically
• Generating reports or dashboards from verification runs

Use other formats for:

• Human-readable (default) - Interactive terminal debugging
• --toon - LLM-assisted debugging, AI tools

Basic Usage

Enable JSON output with the --json flag:

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

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

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

Success Output

When verification succeeds, the output contains an empty failures array:

{
  "schema_version": "2",
  "status": "VALID",
  "failures": [],
  "warnings": [],
  "silicon": {
    "exitCode": 0,
    "stdout": "Silicon finished verification successfully in ?s.\n",
    "stderr": ""
  }
}

The status field is "VALID" and the command exits with code 0.

Failure Output

When verification fails, the output includes detailed failure entries:

{
  "schema_version": "2",
  "status": "INVALID",
  "failures": [
    {
      "failure_id": "d017ca6529e6b16a1b529fbc00c46f8c",
      "failure_kind": "verification",
      "obligation_kind": "postcondition",
      "msg": "Postcondition of increment might not hold.",
      "message": "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;",
      "viper_snippet": "  145 |   ensures $Res == x + 1\n> 146 |   {...}",
      "fix_hints": [
        "Strengthen the implementation or weaken the ensures."
      ],
      "counterexample": null,
      "models": []
    }
  ],
  "warnings": [],
  "silicon": {
    "exitCode": 1,
    "stdout": "Silicon found 1 error in ?s.\n",
    "stderr": ""
  }
}

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

Schema Structure

Top-Level Fields

Field	Type	Description
schema_version	string	Always "2" for current Sector9 versions
status	string	"VALID", "INVALID", or "ERROR"
failures	array	List of verification failure objects
warnings	array	List of warning objects
silicon	object	Raw verifier backend output
error	string?	Error message if diagnostics parsing failed

For frontend translation errors, status is "ERROR" and the silicon object may be absent because Silicon was never invoked. If the Viper backend itself cannot be located, the command exits before JSON verifier diagnostics are produced.

Failure Object Fields

Each failure contains these fields:

Field	Type	Description
failure_id	string	Stable MD5 hash for correlating failures across runs
failure_kind	string	"verification" or "translation"
obligation_kind	string	Type: "assert", "postcondition", "precondition", "invariant", etc.
msg	string	Full error message
message	string	Same as msg (for compatibility)
obligation	string	Short obligation description
method	string?	Function or method name, or null
label	string?	Named assertion label, or null
motoko_span	object?	Source location in the .sr9 file
viper_span	object?	Location in generated Viper code, or null for frontend translation errors
motoko_snippet	string?	Source code excerpt from original file
viper_snippet	string?	Generated Viper code excerpt
fix_hints	array	List of suggested fixes
counterexample	object?	Counterexample models (when --counterexample used)
models	array	Flattened list of all model bindings
contract_snippet	string?	Contract context extracted from the generated Viper failure
source_excerpt	string?	Best available source or Viper excerpt
footprint_missing	object?	Missing reads/modifies clauses
siliconFailure	object?	Raw mapped Silicon failure metadata for verification failures

Span Object Fields

Both motoko_span and viper_span use this structure:

Field	Type	Description
file	string	File path
line	int	Start line (1-based)
col	int	Start column (1-based)
endLine	int	End line
endCol	int	End column

The motoko_span may be null if the failure cannot be mapped back to the original source.

Warning Object Fields

Field	Type	Description
msg	string	Warning message
message	string	Same as msg
code	string	Warning code (e.g., "M0155")
category	string	Warning category
span	object	Source location

Obligation Types

The obligation_kind field indicates what verification obligation failed:

Value	Meaning
postcondition	ensures clause could not be proven
precondition	requires clause not satisfied at call site
assert	assert statement could not be proven
loop invariant	Loop invariant not maintained
invariant	Actor invariant not preserved
insufficient permission	Missing reads or modifies
division by zero	Divisor not proven non-zero

Fix Hints

The fix_hints array contains actionable suggestions:

Obligation	Typical Hints
postcondition	"Strengthen the implementation or weaken the ensures."
precondition	"Guard the call or strengthen the callee requires."
assert	"Add proof steps or strengthen preconditions to establish the assertion."
loop invariant	"Strengthen the loop invariant or add missing assertions."
insufficient permission	"Add missing reads/modifies or ensure permissions are in scope."
division by zero	"Add a requires guard (e.g., d != 0) before division/modulo."

Footprint Analysis

When a permission error occurs, footprint_missing identifies the missing clauses:

{
  "footprint_missing": {
    "reads": ["balance", "owner"],
    "modifies": ["balance"]
  },
  "fix_hints": [
    "Add `reads balance, owner;`",
    "Add `modifies balance;`"
  ]
}

Counterexamples

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

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

The counterexample appears in the failure object:

{
  "counterexample": {
    "models": [
      {
        "label": "return",
        "bindings": [
          {
            "name": "x",
            "value": "0",
            "kind": "local",
            "scope": "local"
          },
          {
            "name": "result",
            "value": "-1",
            "kind": "local",
            "scope": "local"
          }
        ]
      }
    ]
  }
}

Binding Fields

Field	Type	Description
name	string	Variable or field name
value	string	Concrete value from SMT solver
kind	string	"field", "local", or "internal"
scope	string	Scope context
label	string?	Model label (e.g., "entry", "return")

By default, internal bindings (names starting with $) are filtered out unless they appear in the failure message. Use --show-internal with --counterexample to include them.

Translation Errors

For compilation or type errors (not verification failures), the structure differs:

{
  "schema_version": "2",
  "status": "ERROR",
  "failures": [
    {
      "failure_kind": "translation",
      "obligation_kind": "diagnostic",
      "code": "M0057",
      "msg": "unbound variable x",
      "motoko_span": {
        "file": "example.sr9",
        "line": 1,
        "col": 49,
        "endLine": 1,
        "endCol": 50
      },
      "viper_span": null,
      "motoko_snippet": "> 1 | persistent actor { public func f() : async Nat { x } }",
      "viper_snippet": null,
      "source_excerpt": "> 1 | persistent actor { public func f() : async Nat { x } }",
      "counterexample": null,
      "models": []
    }
  ],
  "warnings": []
}

Silicon Backend Output

The silicon object contains raw backend output:

{
  "silicon": {
    "exitCode": 1,
    "stdout": "Silicon 1.1-SNAPSHOT\nSilicon found 1 error in ?s.\n",
    "stderr": ""
  }
}

Timing information is sanitized (replaced with ?s) to ensure reproducible output across runs.

Flag Interactions

The --json flag interacts with other flags:

Flag	Effect
--toon	Mutually exclusive - last one wins
--no-json	Explicitly disables JSON output
--counterexample	Adds counterexample models (does not change format)
--models	Alias for --counterexample
--verify-timeout-ms	Works with JSON; timeout status reflected in output

For human-oriented debugging, see Human-Readable Output. For compact agent input, see TOON Format.

CI/CD Integration

For continuous integration, combine timeout and JSON output:

sector9 --package core ./core/src --verify --json --verify-timeout-ms 300000 my_actor.sr9

Parse the JSON output to integrate with test reporters:

#!/bin/bash
OUTPUT=$(sector9 --package core ./core/src --verify --json file.sr9)
STATUS=$(echo "$OUTPUT" | jq -r '.status')

if [ "$STATUS" = "VALID" ]; then
  echo "Verification passed"
  exit 0
else
  echo "Verification failed"
  echo "$OUTPUT" | jq '.failures[].msg'
  exit 1
fi

Parsing with jq

Extract specific information using jq:

# Get status
sector9 --package core ./core/src --verify --json file.sr9 | jq -r '.status'

# List all failure messages
sector9 --package core ./core/src --verify --json file.sr9 | jq -r '.failures[].msg'

# Get file locations of failures
sector9 --package core ./core/src --verify --json file.sr9 | jq '.failures[] | "\(.motoko_span.file):\(.motoko_span.line)"'

# Count failures
sector9 --package core ./core/src --verify --json file.sr9 | jq '.failures | length'

# Get fix hints
sector9 --package core ./core/src --verify --json file.sr9 | jq -r '.failures[].fix_hints[]'

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

Examples

Successful Verification

$ sector9 --package core ./core/src --verify --json counter.sr9 | jq '.status'
"VALID"

Failed Postcondition with Counterexample

$ sector9 --package core ./core/src --verify --json --counterexample buggy.sr9 | jq '.failures[0]'
{
  "failure_id": "abc123...",
  "failure_kind": "verification",
  "obligation_kind": "postcondition",
  "msg": "Postcondition of withdraw might not hold.",
  "method": "withdraw",
  "motoko_span": {
    "file": "buggy.sr9",
    "line": 12,
    "col": 4
  },
  "fix_hints": [
    "Strengthen the implementation or weaken the ensures."
  ],
  "counterexample": {
    "models": [
      {
        "label": "return",
        "bindings": [
          {"name": "amount", "value": "100", "kind": "local"},
          {"name": "balance", "value": "50", "kind": "field"}
        ]
      }
    ]
  }
}

Multiple Warnings

$ sector9 --package core ./core/src --verify --json file.sr9 | jq '.warnings[] | "\(.code): \(.msg)"'
"M0145: pattern does not cover value false"
"M0237: The compare argument can be inferred"

Summary

• Use --json to enable machine-readable JSON output
• Schema version 2 provides stable, versioned structure
• Includes detailed source locations, snippets, and fix hints
• Add --counterexample to include concrete failing values
• Exit codes match verification status (0 = valid, 1 = invalid)
• Parse with jq or any JSON library for tooling integration
• Backend setup errors such as a missing viperserver.jar are emitted before structured verifier JSON.