Running Verification in CI

Integrate Sector9 verification into your CI/CD pipeline with proper timeout handling, exit code checking, and structured output parsing.

Basic CI Script

A minimal verification script for CI:

#!/bin/bash
set -euo pipefail

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --verify-timeout-ms 300000 contract.sr9

The --verify command returns exit code 0 on success, allowing standard CI failure detection.

Exit Codes

Sector9 uses standard exit codes for CI integration:

Exit Code	Meaning	CI Action
0	Verification succeeded	Continue pipeline
1	Verification failed or type error	Fail build, report errors
2	Invalid arguments or configuration	Fail immediately
124	Outer shell timeout killed the command	Fail with timeout status

Solver timeouts reported through --verify-timeout-ms usually surface as verification failures with timeout text in the diagnostic payload. Exit code 124 is the POSIX convention from the shell timeout command if your CI wraps Sector9 with an outer wall-clock limit.

Recommended Flags for CI

Combine these flags for robust CI verification:

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify \
  --verify-timeout-ms 300000 \
  --cores 4 \
  --deterministic \
  --json \
  contract.sr9

Flag	Purpose
--verify-timeout-ms	Prevent hanging builds (5 minutes recommended)
--cores	Parallelize verification across methods
--deterministic	Reproducible output for caching
--json	Machine-readable results for parsing

Two-Stage Verification

Run type checking first for faster feedback on obvious errors:

#!/bin/bash
set -euo pipefail

# Stage 1: Fast type checking (seconds)
echo "Type checking..."
XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --check contract.sr9

# Stage 2: Full verification (minutes)
echo "Verifying..."
XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --verify-timeout-ms 300000 contract.sr9

Type checking with --check catches syntax and type errors without invoking the SMT solver, providing faster feedback.

Parsing JSON Output

For detailed failure reporting, parse the JSON output:

#!/bin/bash
set -euo pipefail

if ! OUTPUT=$(XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --json --verify-timeout-ms 300000 contract.sr9); then
  true
fi
STATUS=$(echo "$OUTPUT" | jq -r '.status')

if [ "$STATUS" = "VALID" ]; then
  echo "Verification passed"
  exit 0
fi

echo "Verification failed"
echo "$OUTPUT" | jq -r '.failures[] | "\(.motoko_span.file):\(.motoko_span.line): \(.msg)"'
exit 1

The JSON output includes:

• status: VALID, INVALID, or ERROR
• failures: Array of failure details with source locations
• fix_hints: Actionable suggestions when the diagnostic has a known repair

Timeout Handling

Set timeouts appropriate for your codebase:

Complexity	Recommended Timeout
Simple contracts	30 seconds
Moderate complexity	60 seconds
Quantifier-heavy	2-5 minutes
CI pipelines	5 minutes

Handle timeout explicitly:

#!/bin/bash

XDG_CACHE_HOME=/tmp/sector9 timeout 320s ./bin/sector9 --verify --verify-timeout-ms 300000 contract.sr9
EXIT_CODE=$?

case $EXIT_CODE in
  0)
    echo "Verification passed"
    ;;
  1)
    echo "Verification failed"
    exit 1
    ;;
  124)
    echo "Verification command hit the outer CI timeout"
    exit 1
    ;;
  *)
    echo "Unexpected error: $EXIT_CODE"
    exit $EXIT_CODE
    ;;
esac

Parallelization

Use --cores to speed up verification of multi-method contracts:

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --cores 4 --verify-timeout-ms 300000 contract.sr9

The --cores flag sets the verification worker budget; internally the verifier reserves one coordinating process, so --cores 4 gives the backend three parallel workers. Use 2-4 cores for typical CI runners.

Environment Variables

Set cache directory for consistent behavior:

export XDG_CACHE_HOME=/tmp/sector9
./bin/sector9 --verify contract.sr9

This prevents cache-related issues in sandboxed CI environments.

GitHub Actions Example

name: Verify
on: [push, pull_request]

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v5

      - name: Install Sector9
        run: |
          # Your installation steps here

      - name: Type Check
        run: ./bin/sector9 --check src/contract.sr9

      - name: Verify
        run: |
          ./bin/sector9 --verify \
            --verify-timeout-ms 300000 \
            --cores 2 \
            --json \
            src/contract.sr9
        env:
          XDG_CACHE_HOME: /tmp/sector9

Multiple Files

Verify multiple files in a loop:

#!/bin/bash
set -euo pipefail

FAILED=0

for file in src/*.sr9; do
  echo "Verifying $file..."
  if ! ./bin/sector9 --verify --verify-timeout-ms 120000 "$file"; then
    FAILED=1
  fi
done

exit $FAILED

Or use find for recursive verification:

find src -name "*.sr9" -exec ./bin/sector9 --verify --verify-timeout-ms 120000 {} \;

Failure Reporting

Extract failure details for CI reports:

if ! OUTPUT=$(XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --json contract.sr9); then
  true
fi

# Count failures
FAILURE_COUNT=$(echo "$OUTPUT" | jq '.failures | length')
echo "Found $FAILURE_COUNT verification failures"

# List failure locations
echo "$OUTPUT" | jq -r '.failures[] | "- \(.motoko_span.file):\(.motoko_span.line): \(.obligation_kind): \(.msg)"'

# Show fix hints
echo "$OUTPUT" | jq -r '.failures[].fix_hints[]?' | sort -u

Summary

• Use --verify with --verify-timeout-ms to prevent hanging builds
• Check exit codes: 0 = pass, nonzero = fail; 124 means an outer timeout wrapper killed the process
• Run --check first for fast feedback on type errors
• Use --json for machine-readable output in complex pipelines
• Set --cores for parallel verification on multi-method contracts
• Use --deterministic for reproducible builds and caching
• Keep XDG_CACHE_HOME stable inside a CI job so verifier cache paths are predictable