Sabba: A Security Tool That Proves Bugs by Actually Running Them

Sabba is an MCP server and CLI that coding agents like Claude Code, Codex, and Cursor can call to find and verify security bugs. Instead of asking a language model whether code is vulnerable — a near coin-flip prone to false positives — Sabba has the model propose candidate inputs, then an execution oracle compiles and runs them. A finding is only reported if the exploit actually reproduces.

The tool ships provers across multiple domains: clang with AddressSanitizer/UBSan for C/C++, Foundry mainnet forks for Solidity/EVM, atheris for Python, native fuzzing for Go, and Jazzer-based provers for Java and Node.js. Its fuzzing components are designed to be "harness-untrusted" — even if the target code tries to game the fuzzing harness, verdicts are read from channels that can't be forged, such as a real exception's stack trace or a parent process's measurement of a killed child.

As a demonstration, Sabba reproduced two known cJSON vulnerabilities (a stack exhaustion and a heap over-read) directly from their upstream fix commits, packaging each as a re-runnable proof bundle rather than claiming novel zero-day discovery. The project also supports local models and uses a three-tier reasoning cascade — free heuristics, a local model, then a frontier model only for hard cases — while keeping the same verification rule at every tier, so cheaper tiers cost coverage, never soundness.