Skip to main content

Installation and Setup

Sector9 is distributed as a container image. You do not need a repository checkout, Nix, OCaml, Java, Viper, or Z3 installed on your machine; those tools are bundled in the image.

The examples below use the public GHCR image:

ghcr.io/neutrinomic/sr9:latest

Use the tag named in the release notes when you want a pinned release. Use latest when you want the newest published image.

Prerequisites​

Install one container runtime:

  • Docker Engine or Docker Desktop
  • Podman, if your environment standardizes on Podman

The wrapper below uses Docker by default. With Podman, run commands as SECTOR9_CONTAINER=podman ./sr9 ....

Codex CLI Skill​

Download skill.md

Install path:

${CODEX_HOME:-$HOME/.codex}/skills/sector9/SKILL.md

Pull the Image​

docker pull ghcr.io/neutrinomic/sr9:latest

Create ./sr9​

Create this wrapper in your project:

cat > sr9 <<'EOF'
#!/usr/bin/env bash
set -euo pipefail

IMAGE="${SECTOR9_IMAGE:-ghcr.io/neutrinomic/sr9:latest}"
ENGINE="${SECTOR9_CONTAINER:-docker}"
USERNS_ARGS=()
EXTRA_ARGS=()
ENV_ARGS=()

if [ "${SECTOR9_USERNS_KEEP_ID:-0}" = "1" ]; then
  USERNS_ARGS=(--userns=keep-id)
fi

if [ -n "${SECTOR9_RUN_ARGS:-}" ]; then
  # shellcheck disable=SC2206
  EXTRA_ARGS=(${SECTOR9_RUN_ARGS})
fi

if [ -n "${SILICON_FLAGS:-}" ]; then
  ENV_ARGS=(-e "SILICON_FLAGS=$SILICON_FLAGS")
fi

exec "$ENGINE" run --rm \
  "${USERNS_ARGS[@]}" \
  "${EXTRA_ARGS[@]}" \
  "${ENV_ARGS[@]}" \
  --user "$(id -u):$(id -g)" \
  -v "$PWD:/work" \
  -w /work \
  "$IMAGE" "$@"
EOF

chmod +x sr9

Supported Architectures​

The published image supports both linux/amd64 and linux/arm64. Docker Desktop on Apple Silicon and ARM64 Linux hosts should pull the ARM64 image automatically. x86-64 Linux hosts should pull the AMD64 image automatically.

Use the native image for normal verification. For example, use linux/arm64 on Apple Silicon and ARM64 Linux, and linux/amd64 on x86-64 Linux. Forcing linux/arm64 on an x86-64 host runs through QEMU emulation and can be much slower than native execution.

If your runtime warns that the image platform does not match your host, use the native image.

Run Sector9​

./sr9 --verify src/main.sr9

The wrapper mounts your current directory at /work, so relative paths work from your project root.

Example​

Write a small verified actor and verify it:

cat > counter.sr9 <<'EOF'
persistent actor {
  var counter : Nat = 0;

  public func increment() : async Nat
    modifies counter
    ensures counter == old(counter) + 1;
    ensures result == counter;
  {
    counter += 1;
    counter
  };
}
EOF

./sr9 --verify counter.sr9

Common Commands​

# Whole-imported-world source hygiene check, no SMT solving
./sr9 --check file.sr9

# Full Viper verification
./sr9 --verify file.sr9

# Emit generated Viper
./sr9 --deterministic --viper file.sr9

Export docs & examples​

The image also contains the documentation text files, runnable examples, and the Sector9 core library sources. Export them when you want local reference material:

mkdir -p .sr9docs
./sr9 docs export .sr9docs

After export, your host directory contains:

.sr9docs/
├── docs/       # Docusaurus text pages from docs/docs
├── examples/   # Example .sr9 files from docs/examples
└── core/       # Read-only reference copy of the core library sources

Example verification sidecars such as .verify and .check are intentionally omitted. The exported core/ tree is for reading and searching; the image already passes its in-image core package to sector9 automatically when you run verification.

For advanced workflows, the fixed in-image paths are:

  • Documentation and examples: /opt/sector9/docs
  • Core library package: /opt/sector9/core/src
./sr9 docs path

Write Output Files​

The wrapper runs the container with your host UID/GID, so generated files are writable by you:

./sr9 -c test.sr9 -o test.wasm

With Podman:

SECTOR9_CONTAINER=podman ./sr9 --check test.sr9

If bind mounts still produce permission errors, add: SECTOR9_USERNS_KEEP_ID=1.

Core Library Imports​

The image includes core/src and automatically injects:

--package core /opt/sector9/core/src

That means imports such as this work without extra flags:

import Nat "mo:core/Nat";

The image is intentionally mo:core oriented. It does not bundle mo:base; prefer mo:core/... imports in Sector9 examples and new projects.

CPU and Memory Limits​

Sector9 can use multiple verifier workers, but Docker must make those resources available to the container.

Use both flags when you want parallel verification:

  • SECTOR9_RUN_ARGS="--cpus=N" controls how many host CPUs the container may use.
  • Sector9 --cores N controls how many verifier threads Sector9 asks the backend to use.
SECTOR9_RUN_ARGS="--cpus=8" ./sr9 --verify --cores 8 file.sr9

If verification runs out of memory, raise the container memory limit:

SECTOR9_RUN_ARGS="--cpus=8 --memory=12g" ./sr9 --verify --cores 8 file.sr9

On Linux Docker Engine, containers can usually use host resources unless you set limits. On Docker Desktop, also increase the VM resources in Settings → Resources; per-command flags cannot exceed the CPU and memory assigned to Docker Desktop. On Podman machine setups, increase the machine resources first, for example:

podman machine stop
podman machine set --cpus 8 --memory 12288
podman machine start

Use fewer Sector9 cores than available CPUs if the machine becomes memory-bound. Each parallel verifier worker adds memory pressure.

Troubleshooting​

docker: command not found​

Install Docker Desktop, Docker Engine, or Podman. Sector9 itself does not require a local compiler toolchain when you use the image.

pull access denied or manifest unknown​

Check the image name and tag. The public image is ghcr.io/neutrinomic/sr9:latest; release notes may name a more specific tag. If the name is correct, retry after docker logout ghcr.io in case an old GHCR login is hiding public packages.

Permission denied writing output files​

The wrapper already runs the container as your host UID/GID. If bind-mounted directories still fail under Podman or a rootless engine, run: SECTOR9_USERNS_KEEP_ID=1 ./sr9 ....

mo:base/... import not found​

The runtime image bundles mo:core, not mo:base. Change imports to mo:core/... or use dependencies explicitly supplied by your project.

Z3 canceled when forcing ARM64 on x86-64​

If you run the ARM64 image under QEMU emulation on an x86-64 host, Silicon's small internal SMT timeouts can expire before Z3 responds. Prefer the native AMD64 image on x86-64 hosts. If you are specifically testing the ARM64 image under emulation, increase Silicon's internal timeouts:

SILICON_FLAGS='--checkTimeout 10000 --z3SaturationTimeout 10000' \
SECTOR9_RUN_ARGS='--platform linux/arm64' \
./sr9 --verify-timeout-ms 600000 --cores 1 --verify test.sr9

Next Steps​

Summary​

  • Install Docker or Podman, not the Sector9 repository
  • Pull the published Sector9 CLI image
  • Create ./sr9
  • Use --check for source/import hygiene and --verify for full Viper verification
  • Export bundled docs and examples with ./sr9 docs export .sr9docs