This guide takes a repository that already has working Soroban contracts and adds Sanctifier to it in three stages:
- First scan — install the CLI and see where you stand.
- Baseline — capture a known-good report and a README badge.
- CI gate — fail pull requests that introduce critical/high findings.
It assumes nothing has been configured yet. By the end you will have a
.sanctify.toml, a committed baseline report, and a CI job that blocks
regressions. This page is part of the core documentation set; pair
it with the Configuration Reference and the
CLI Reference.
Prerequisites: a Rust toolchain (
rustc/cargo), and your contracts build withcargo build. Theverify/provecommands additionally need the Z3 SMT solver installed — see Installing Z3.
From a clone of this repository:
cargo install --path tooling/sanctifier-cliThis puts a sanctifier binary on your PATH. Confirm it:
sanctifier --helpPoint analyze at a contract crate (a directory containing Cargo.toml, or the
workspace root). Paths default to .:
cd /path/to/your/soroban-repo
sanctifier analyze ./contracts/my-tokenYou will get a human-readable report of authorization gaps, panics, unchecked
arithmetic, ledger-size risks, and upgrade-pattern issues. Each finding maps to a
stable code (S001…S016) documented in Finding Codes; the
underlying terms are defined in the Glossary.
Exit codes: in the default text mode,
analyzeis informational and exits0even when it finds problems. To make a scan fail on critical/high-severity findings, use JSON mode (--format json) — see Stage 3. This distinction is what lets you adopt Sanctifier gradually without breaking your build on day one.
Drop a starter .sanctify.toml into your repo root so the tool's behaviour is
explicit and version-controlled:
sanctifier init # add --force to overwrite an existing fileOpen the file and tune it using the Configuration Reference.
At minimum, set ignore_paths to skip vendored
or generated code, and decide on a ledger_limit
and whether to enable strict_mode.
Commit the file:
git add .sanctify.toml
git commit -m "chore: add Sanctifier configuration"A baseline is a machine-readable snapshot of the current findings. It lets you (a) track progress as you fix issues and (b) render a status badge.
sanctifier analyze . --format json > sanctifier-report.jsonInspect it (the report includes a full error_codes map plus per-category
findings):
jq '.summary, .error_codes' sanctifier-report.jsonDecide what to do with the report:
- Triage now: fix the critical/high findings before wiring CI, so the gate in Stage 3 passes immediately.
- Adopt gradually: commit
sanctifier-report.jsonas a baseline artifact and open follow-up issues for each finding, then turn the gate on once the count is manageable.
Turn the JSON report into an SVG badge and a Markdown snippet:
sanctifier badge \
--report sanctifier-report.json \
--svg-output badges/sanctifier-security.svg \
--markdown-output badges/sanctifier-security.mdPaste the generated Markdown into your README so the security status is visible.
See badge for all flags (including --badge-url for
hosting the SVG).
If you want formal guarantees, annotate token-style contracts with
#[sanctify::invariant(...)] and check them:
sanctifier verify ./contracts/my-tokenSee the README invariants example and
contracts/token-invariants for a complete reference.
Now make pull requests fail when they introduce critical or high-severity
findings. The key fact from Stage 1: analyze --format json exits non-zero
when there are critical/high findings, which is exactly what a CI step needs.
Add .github/workflows/sanctifier.yml:
name: Sanctifier Security
on:
pull_request:
push:
branches: ["main"]
jobs:
sanctify:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Install Rust
uses: dtolnay/rust-toolchain@stable
# Required only if you also run `verify`/`prove` (Z3 SMT backend).
- name: Install Z3
run: sudo apt-get update && sudo apt-get install -y libz3-dev
- name: Install Sanctifier
run: cargo install --path tooling/sanctifier-cli
# If Sanctifier lives in another repo, install from there instead, e.g.
# cargo install --git https://github.com/Centurylong/sanctifier sanctifier-cli
- name: Static analysis (fails on critical/high findings)
run: sanctifier analyze . --format json > sanctifier-report.json
- name: Upload report
if: always()
uses: actions/upload-artifact@v4
with:
name: sanctifier-report
path: sanctifier-report.json
# Optional: fail if any declared invariant is refuted or unknown.
- name: Verify invariants
run: sanctifier verify ./contracts --strictThe third step is the gate: a critical (e.g. missing require_auth) or high
(e.g. unchecked arithmetic, ledger size exceeded) finding makes the job exit
non-zero and blocks the merge. The verify --strict step adds a stronger gate
for contracts that declare invariants.
-
Set
strict_mode = truein.sanctify.tomlto fail when state reaches 90% of the ledger limit. -
Lower
approaching_thresholdfor earlier ledger-size warnings. -
Add project-specific
custom_rules(reported asS007) to ban patterns your team has agreed to avoid. -
Add a
provesmoke check for token invariants:sanctifier prove --invariant supply_conserved --no-save
The verify and prove commands use the Z3 SMT solver. analyze, badge,
init, and callgraph do not require it.
| Platform | Command |
|---|---|
| Ubuntu/Debian | sudo apt-get install -y libz3-dev |
| macOS (Homebrew) | brew install z3 |
| Fedora | sudo dnf install z3-devel |
If the build cannot find z3.h (common on macOS), point the bindings at your
install, e.g.:
export Z3_SYS_Z3_HEADER="$(brew --prefix z3)/include/z3.h"See the FAQ for more build-error fixes.
Sanctifier is additive and does not modify your contracts. To remove it:
rm .sanctify.toml sanctifier-report.json
rm -f .github/workflows/sanctifier.yml
cargo uninstall sanctifier-cli- Configuration Reference — every
.sanctify.tomlkey. - CLI Reference — every command and flag used above.
- FAQ & Troubleshooting — fixes for common adoption problems.
- Finding Codes — what each
S0xxcode means. - Glossary — definitions for the security terms referenced here.