2akouwu/reverify

Reverify – deterministic verification for AI‑generated binary analysis

What it is – A pure‑Python (with optional native extensions) toolkit that lets a language model propose facts about a binary (or source code) and then checks those facts against the actual file. The verifier returns VERIFIED, REFUTED or INCONCLUSIVE together with concrete evidence (bytes, disassembly, emulation results, etc.).

Why it matters – Large language models are good at reading code but often hallucinate when asked to reverse‑engineer binaries: they invent struct offsets, function prologues, API names, etc. Reverify makes the model’s claims grounded by running deterministic analyses (PE/ELF/Mach‑O parsing, disassembly, pattern‑matching, CPU emulation, Protobuf parsing, Frida hook generation, and optional Z3/angr proofs). A claim is only accepted if the tool can demonstrate it on the real bytes, eliminating the biggest source of error in AI‑assisted reverse engineering.

Core capabilities

• Deterministic core – pure‑Python parsers and disassemblers for PE, ELF, Mach‑O; x86/x64/ARM/ARM64 disassembly; AOB scanning; lightweight CPU emulator; protobuf/TLV parsing; Frida hook generation. No external binaries required.
• Optional full‑stack back‑ends – pip install "reverify[full]" adds Capstone (high‑performance disassembly), Unicorn (real CPU emulation), LIEF (binary parsing) and Z3 (formal proofs). pip install "reverify[angr]" adds angr for call‑graph and cross‑reference analysis. The tool falls back to the pure‑Python core if these are not installed.
• Verification loop – Users supply a claim (JSON describing the expected bytes, instructions, emulated register state, exported symbols, etc.). Reverify checks the claim against the binary and returns a verdict plus a receipt containing the binary’s SHA‑256, tool versions, and evidence.
• Weighting & information score – Each verified claim is assigned a weight based on how informative it is (entropy, uniqueness). A reconstruction is considered grounded only when no claim is refuted and the total weight exceeds a configurable threshold (--min-information).
• Ledger & rollover – Verified facts and known‑false claims are persisted to .reverify/ledger/<sha256>.json. When an AI agent’s context window is about to overflow, reverify rollover writes a hand‑off file containing only the verified facts, allowing the next session to start fresh without losing trustworthy state.
• Agent‑native MCP server – Reverify can run as an MCP (Model‑Control‑Protocol) server, so Claude Code, Cursor, Gemini CLI, OpenCode, or any OpenAI‑compatible agent can call the verification functions directly. A plain CLI is also provided.
• Equivalence testing – reverify equiv <reference> <candidate> runs both implementations on the same inputs and checks that outputs match, useful for verifying AI‑generated refactorings of source code.

Typical workflow

# Install core (or with full back‑ends)
pip install reverify          # pure‑Python only
pip install "reverify[full]"   # adds capstone, unicorn, lief, z3

# Quick automatic analysis of a binary
reverify auto sample.bin --json

# Verify a specific claim
reverify verify sample.bin --claim '{
  "kind": "instructions",
  "offset": 4096,
  "mnemonics": ["push","mov","sub"],
  "note": "function prologue"
}'

# Run a multi‑step session with an LLM driver
reverify orchestrate target.exe \
  --goal "map the loader: entry, imports it really uses, exports" \
  --driver claude

Benchmarks – On 71 real Windows system files, a language model’s textbook‑style prologue claim was wrong 97 % of the time. Reverify refuted every incorrect claim and never incorrectly verified a false claim (0/71). The benchmark runs automatically in CI on Linux, macOS and Windows, and the results are published in BENCHMARK.md.

Installation & usage – The package is on PyPI (pip install reverify). The core works with only the Python standard library; optional native back‑ends are pulled in via extras. The CLI can be invoked directly from a checkout (python reverify/cli.py …).

Safety & licensing – Intended for authorized reverse engineering (malware analysis, CTF, interoperability research, or software you own). Licensed under MIT; CI includes fuzzing and extensive cross‑platform testing. Receipts and SLSA provenance attestations are provided for reproducible audits.

---

Reverify therefore provides a concrete, deterministic guard that lets AI agents safely assist in binary reverse engineering and source‑code equivalence checking without trusting the model’s hallucinations.