SABBA v0.2.1

First release available from PyPI:

pip install sabba
sabba verify cwe121_stack_overflow

That second command proves a real stack buffer overflow with no clone, no model and no API key,
because the demo targets now ship inside the package.

Soundness fixes in the C and C++ oracle

Read this part if you use verify or prove, because it changes what counts as a finding.

A bare fatal signal is no longer verified. The oracle used to verify any signal it saw when
no sanitizer fired. The signal a PoC most often earns is SIGABRT from assert() or abort(),
and a defensive assertion refusing bad input is hardening rather than a vulnerability, so that
rule turned target robustness checks into confirmed findings. Such a run now returns
signal_unconfirmed and is surfaced as an unverified candidate, the same way a hang already
was. Every managed prover already required an attributed frame before calling a signal
native_crash; the C path now matches them.

The vulnerability class comes off the sanitizer's own error line. It used to be matched
anywhere in stderr, which the target also writes to, so a program that logged "guarding against
double-free" while UBSan reported a signed integer overflow was filed as a double-free.

Both are covered by regression tests. If you were relying on crash_signal verdicts, expect
fewer findings and more candidates, which is the intended direction.

Packaging

The demo targets moved under sabba/ so they ship in the wheel, and a target argument resolves
either as a path or as the bare name of a bundled target. An existing path always wins, so a
directory of your own is never shadowed by a bundled name. A missing target now lists what is
available instead of raising a traceback.

Full test suite: 303 passed, 11 skipped.

SABBA v0.2.0

First public release of Sabba, a security and correctness prover that any coding agent can call over MCP. Nothing is reported unless it runs: a finding is a re-runnable proof, not a score.

What is in it

• 14 MCP tools, most token-free. verify_change proves a change works through the bundled Magga engine: a newly added test fails on the git base and passes on the head, across 16 languages. prove, hunt, scan, verify, and solve find and prove security bugs, minting a finding only when the exploit reproduces inside the target.
• Provers per language and chain: C/C++ (clang + AddressSanitizer/UBSan), Solidity/EVM (Foundry mainnet fork), Python (atheris), Go, Java (Jazzer), and Node/JS/TS (Jazzer.js).
• A scope-gated Kali toolchain layer with an append-only audit log, a network-cut container sandbox, and installable security command templates.
• Codex, Claude Code, OpenCode, Cursor, and Hermes all connect over stdio or HTTP.

Install

git clone --recurse-submodules https://github.com/8NobleTruths/sabba.git
cd sabba && ./install.sh

Then wire it into Codex via ~/.codex/config.toml, or any MCP client. See the README and docs/AGENT_INTEGRATION.md.