Security Templates CLI & MCP Server for coding agents that prove every finding by running it.
Claude Code, Codex, OpenCode, Cursor, and Hermes call Sabba to prove a change, find and prove bugs, vet a skill, and drive the security toolchain, authorized-scope-only.
If it does not run, Sabba does not report it.
Two real cJSON vulnerabilities, reproduced and proved by running them: a stack exhaustion
(CWE-674, fixed upstream in 2017) and a heap over-read in parse_object
(CWE-125, fixed in 2024). Both came out of variant analysis from the upstream fix commits, so they are reproductions of known bugs and not new discoveries. What Sabba contributes is the proof: each write-up in docs/scans carries the exact input and a bundle you can re-run on your own machine to watch AddressSanitizer fire. Novel zero-day discovery is a later phase and is not something this repository claims yet.
That is the whole design. Most tools that use a language model ask it "is this function vulnerable?" That is close to a coin flip, even for large models, and unverified guesses bury maintainers in false positives. Sabba takes the opposite stance: a model proposes candidates, but an execution oracle runs an exploit and decides whether a security property actually broke. Nothing is reported unless the exploit reproduces. A finding is not a score, it is a re-runnable proof.
Sabba runs as an MCP server, so Claude Code, Codex, OpenCode, Cursor, and Hermes can call it.
For Codex CLI, add it to ~/.codex/config.toml
:
[mcp_servers.sabba]
command = "sabba"
args = ["mcp"]
For Claude Code:
claude mcp add sabba -- sabba mcp # after installing; see Install below
Fourteen tools, most token-free: ** verify_change** (prove a change works in any of 16 languages: a new test fails on the base and passes on the head, via the bundled Magga engine) and
(the same differential, run natively for C/C++/EVM),
prove
verify
/ solve
/
hunt
/ scan
(find and prove bugs), (vet a skill by running it under observation),
security_scan
rank
, run_sandboxed
, and (drive nmap / nuclei / ffuf / sqlmap and the rest, scope-enforced and sandboxed). Install the security command templates with
kali_run
sabba templates install
. Full catalog and per-client configs in docs/AGENT_INTEGRATION.md.
Correctness and security in one server. verify_change
proves the change does what it
claims; prove
/ hunt
/ scan
prove it added no new bug. The change-verification engine is
Magga, vendored as a submodule under magga/
and
driven through npx
, so both halves ship as one tool.
Find a real bug and hand you the proof, not a hunch. Every finding ships as a bundle: the input that triggers it, the target, the command that reproduces it, and the sanitizer output it produced. You do not have to trust the report, you can re-run it. The cJSON bugs above are two of these bundles.
Work across languages and across chains, with one rule. The oracle started on C and C++ memory safety and generalized into a registry of provers, one per runtime and vulnerability class. Every prover obeys the same contract: a finding is minted only from a verdict that a real, security-relevant crash happened inside the target.
| Domain | Runtime it proves on | What counts as proven | Examples |
|---|---|---|---|
| C / C++ | |||
| clang + AddressSanitizer / UBSan | the sanitizer reports a real memory error | heap / stack overflow, use-after-free | |
| Solidity / EVM | |||
| Foundry mainnet fork | attacker ETH profit or a broken solvency invariant, measured on-chain | reentrancy fund-drain | |
| Python | |||
| atheris | a crash raised in the target, not the harness | stack exhaustion, C-extension segfault | |
| Go | |||
go test -fuzz |
|||
| a recovered runtime panic at a target frame | index / slice out of range, nil deref | ||
| Java / JVM | |||
| Jazzer | a target throwable or a bug-detector finding | stack overflow, injection detectors | |
| Node JS / TS | |||
| Jazzer.js | a target crash or a bug-detector finding | prototype pollution, ReDoS, path traversal |
Refuse to be fooled, even by a hostile harness. When a model writes the fuzz harness, a hostile target could try to steer it into faking a crash. Sabba's fuzzing provers are harness-untrusted: the fuzzer only discovers a candidate input, then a Sabba-owned reproducer re-runs it and reads the verdict from channels the harness cannot forge (a real exception's structured stack, or the parent's own measurement of a killed child). It reads no stdout, no artifact file, no magic phrase. The full model is in docs/PROVER_SOUNDNESS.md.
Prefer soundness over coverage, and say so. Where a crash cannot be soundly pinned to the target (a hang or an out-of-memory that could just as easily be the harness spinning or pre-filling the heap), Sabba surfaces it as an unverified candidate for a human, but never mints it as a finding. It would rather miss a bug than report one that did not happen.
Meet you where you work. One command, several surfaces: a scriptable CLI (verify
,
solve
, hunt
) and an interactive REPL (pictured above) that streams the model, runs tools,
and renders each proof as a card. Running sabba
with no arguments opens the REPL.
The oracle and provers never needed a model, and the model-driven parts can run on your own
machine too. Point the reasoning at a local, OpenAI-compatible endpoint with
SABBA_LLM_BACKEND=local
, and train a small CPU risk ranker so retrieval looks at the risky functions first:
sabba mltrain # trains a risk ranker (TF-IDF + logistic), saved to ~/.sabba
A three-tier cascade keeps work cheap: Reflex (no model: the ranker, Z3, the oracle), Resident (the local model), and Teacher (a frontier model) only for the hard cases. The verdict rule holds across tiers, so a cheaper tier costs coverage, never soundness. See docs/LOCAL_ML.md.
model / z3 / retrieval -> candidate input
|
v
+---------------------------------------+
| execution oracle / prover |
| compile, run the exploit, measure |
+---------------------------------------+
| |
reproduces does not
| |
FINDING dropped
The oracle is the one gate. Whether a candidate came from the Z3 synthesizer or from the model, it is compiled and run before anything is reported. Z3 proposes an input, the oracle decides. The model proposes an input, the oracle decides. The same discipline carries to every domain in the table above: on an EVM fork the chain measures the attacker's profit, not the model, so the model cannot grade its own work.
pip install sabba # or: pipx install sabba / uvx sabba mcp
Then run sabba doctor
to see what the toolchain can prove on this machine. verify_change
shells out to the Magga engine over npx
, so it needs Node on your PATH but no extra install step.
To work on Sabba itself, clone it with the submodule and use the installer, which sets up an
isolated environment under ~/.sabba
and puts a sabba
command on your PATH:
git clone --recurse-submodules https://github.com/8NobleTruths/sabba.git
cd sabba
./install.sh
Update later with sabba update
, remove with sabba uninstall
.
Provers use the toolchain of the domain you target: clang with AddressSanitizer for C and
C++, Foundry for EVM, and atheris, go
, Jazzer, or Jazzer.js for the managed languages.
sabba doctor
reports what is present.
sabba # opens the REPL; type /setup for guided first-run setup
sabba verify cwe121_stack_overflow
sabba solve cwe121_stack_overflow
Those two names are demo targets that ship inside the package, so an installed Sabba can prove
a real bug on the first command, with no clone, no model, and no API key. Point the same
commands at a directory of your own holding a target.json
to work on your code instead.
First run opens a guided setup: /setup
shows a checklist, and each step explains why it is
worth doing, what happens if you skip it, and what happens when you do it. /local-llm-config
detects your CPU and RAM, recommends a Qwen2.5-Coder size, and pulls it with Ollama so the
model runs on your machine; /add-model-key
uses a cloud model instead; /ml-config
trains
the risk ranker. You can select any command from the /
menu. /solve
and /verify
prove bugs with no model at all, so they work before any setup.
Bring in a model through OpenRouter (or any OpenAI-compatible endpoint) to hunt fresh code:
export SABBA_LLM_BACKEND=openrouter
export OPENROUTER_API_KEY=... # from openrouter.ai/keys
sabba hunt cwe122_heap_overflow --model qwen/qwen-2.5-coder-32b-instruct
Keys are read from the environment, never stored in the repo, and a pre-commit hook blocks anything that looks like a credential (see CONTRIBUTING.md).
docs/SABBA_AGENT_DESIGN.md- the C and C++ bug-finder: the oracle, retrieval, the Z3 synthesizer, and the reasoning agent.docs/PROVERS_MULTI_DOMAIN_DESIGN.md- how the oracle generalizes into the prover registry, including Web3 and Solidity.docs/PROVER_SOUNDNESS.md- the harness-untrusted verification model that makes the fuzzing provers sound against an adversarial harness.docs/WATER_LAYER_DESIGN.md- the next layer: an agent that keeps its skills as runnable code, runs without a frontier model, and can be rebuilt from a seed. Provers are the skills it accumulates.
The native oracle, retrieval, Z3 synthesis, the reasoning agent, and the full prover registry across C/C++, Solidity/EVM, Python, Go, Java, and Node run today, each with live proofs. The Water Layer and a broader symbolic-execution pass are next.
Apache-2.0. See LICENSE. The framework is open source. Trained model weights and datasets are developed separately and are not part of this repository.