Getting Started

Install the prebuilt binary for your platform and run your first analysis in under a minute.

Install

Windows (x64)

Download saple-windows-x64.zip, unzip it, and add the folder containing saple.exe to your PATH.

# Verify the install
saple --version

macOS

Download saple-macos.dmg, double-click it to mount, then either run the bundled install.sh or drag saple into a directory on your PATH:

sudo install -m 0755 /Volumes/SAPLE/saple /usr/local/bin/saple
saple --version

On first run, macOS may prompt about an unsigned binary — open System Settings → Privacy & Security and click Open Anyway.

Linux (Ubuntu, Debian)

Download saple-linux-x64.deb and install with apt:

sudo apt install ./saple-linux-x64.deb
saple --version

Linux (CentOS, RHEL, Fedora)

Download saple-linux-x64.rpm and install with rpm or dnf:

sudo rpm -i saple-linux-x64.rpm
saple --version

The Linux binary is fully static (musl libc, Z3 bundled) — no system dependencies.

Your first analysis

SAPLE ships with example specifications. Try the dining philosophers:

saple analyze examples/dining_philosophers.sbl --verbose

The analyzer verifies three properties: noDeadlock, mutualExclusion, and progress.

CLI commands

saple parse — Parse and display AST

saple parse examples/dining_philosophers.sbl
saple parse examples/dining_philosophers.sbl --format json

saple analyze — Vulnerability analysis

The main command. Derives all detection from the SPL specification itself — zero hardcoded CWEs.

# Basic
saple analyze examples/dining_philosophers.sbl

# Full execution trace
saple analyze examples/dining_philosophers.sbl --trace

# Extract reusable rules and export
saple analyze examples/dining_philosophers.sbl \
  --extract-rules --export rules.json

Key flags

saple model — Symbolic state-space exploration

saple model examples/network_protocol_stack.sbl --mode forward
saple model examples/network_protocol_stack.sbl --mode backward --max-steps 200

saple match — Pattern matching

saple match examples/dining_philosophers.sbl --pattern patterns/deadlock.sbl

saple test — Test generation

saple test examples/dining_philosophers.sbl
saple test examples/dining_philosophers.sbl --coverage state
saple test examples/dining_philosophers.sbl --coverage path

saple translate — Translate to SPL

Translate from a supported input representation into SPL:

• x86-64 assembly
• ARM64 / AArch64 assembly
• Clang / LLVM IR (C, C++, Rust front-ends)
• VHDL hardware description
• Blockchain smart contract source

saple translate firmware.s   --arch x86-64    --output firmware.sbl
saple translate binary.s     --arch arm64     -o binary.sbl
saple translate module.ll    --arch clang     -o module.sbl
saple translate design.vhd   --arch vhdl      -o design.sbl
saple translate contract.vy  --arch blockchain -o contract.sbl

Next steps