Reverify

The AI proposes. The bytes decide.
Anti-hallucination for AI agents that read binaries: every claim is checked against the real bytes.

Ask an AI to reverse-engineer a file and it will make things up — offsets, structs, what the code does — and say it like it's fact. Reverify checks it against the one thing that can't lie, the bytes. Every claim is tested against the real binary; only what's true survives.

On 19 real Windows system files, the AI's textbook answer was wrong 100% of the time — reverify caught every one, with zero false alarms (EXAMPLE.md, BENCHMARK.md; python benchmarks/prologue_prior.py).

The problem

Language models are great at reading code and unreliable at reverse engineering. Ask a model to reconstruct a struct or an algorithm from a binary and it will confidently invent offsets, sizes, and behavior. In binary analysis this hallucination problem is far worse than in source code, and "did the model just make that up?" is the single biggest blocker to using AI for real RE.

What Reverify does

Reverify pairs a language model with a deterministic, pure-Python RE toolkit and makes the toolkit the judge. The model proposes; the tools verify. A hypothesis about a structure or an algorithm is only reported once it has been checked against the actual bytes — disassembled, pattern-matched, or executed in the emulator — so the output is grounded in the binary instead of the model's imagination.

• Deterministic core — PE/ELF/Mach-O parsing, x86/x64/ARM/ARM64 disassembly, AOB pattern scanning, CPU emulation, Protobuf/TLV dissection, Frida hook generation. Pure Python out of the box; installs clean with no Ghidra.
• Mature engines, optional — with pip install "reverify[full]" the toolkit upgrades itself in place to capstone (disassembly), unicorn (real CPU emulation), lief (PE/ELF/Mach-O) and Z3 (proofs); pip install "reverify[angr]" adds angr for function boundaries, the call graph and cross-references. Not installed? It falls back to the pure-Python core. reverify backends shows what's active.
• Grounded, not guessed — structural claims are verified against the binary by the tools.
• Agent-native — ships as an MCP server, so Claude Code, Cursor, and other agents can call the tools directly; also a plain CLI.

Reverify is for authorized reverse engineering — malware analysis, CTF, interoperability research, and software you own or are permitted to analyze. See SECURITY.md.

Quick start

# Install the CLI + MCP server from PyPI:
pip install reverify        # pure-Python core; or "reverify[full]" for capstone+unicorn+lief
reverify auto sample.bin --json

# Or run straight from a checkout — pure standard library, nothing to install:
python reverify/cli.py auto sample.bin --json
python reverify/cli.py parse-pe sample.exe --json
python reverify/cli.py disasm 90505831C0C3 --arch x86_64

The verification loop

This is what the name is about. A claim is any hypothesis about the binary; the deterministic tools are the judge and hand back VERIFIED, REFUTED, or INCONCLUSIVE together with the bytes they actually observed:

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

# Check a reconstructed routine actually computes what the model claimed:
reverify verify - --claim '{
  "kind": "emulate_result", "code": "b805000000b90300000001c8c3",
  "arch": "x86", "expect_registers": {"eax": 8}
}'

Claims can be batched from a JSON file (--claims-file claims.json); the CLI exits non-zero if anything is refuted, so an agent or CI job can gate on a grounded reconstruction. Claim kinds: bytes_at, u16_at / u32_at / u64_at (typed reads, no endianness math), pattern_present, string_present, instructions (mnemonics and optionally operands), emulate_result, behavior_equiv, prove_equiv, protobuf_field, import_present, export_present, section_present, and the semantic kinds function_at, calls, references, reachable_from_entry (see The semantic layer). Offsets are file offsets unless a claim says "space": "rva" or "va"; the verifier translates through the section table and echoes all three addresses in the evidence, and a refuted bytes_at reports where the expected bytes actually are. Set "observe": true (or omit expected) to have the tools read a value instead of asserting one, and "depends_on": [...] so a refuted root invalidates the claims built on it.

Grounded means informative, not just "nothing refuted"

"Every claim verified" is trivially reachable: assert that the file starts with MZ and that .text exists. So Reverify also weighs how much a verified set actually says. Each result carries a weight — zero for claims that merely restate the fact sheet the model was shown, for duplicates, for inline code/data that does not occur in the binary (self-referential), and for echoes of the tools' own previous output; otherwise it is measured from the binary itself — how often the expected content occurs in this file and how much entropy it has — so zero padding, a ubiquitous prologue, or a pattern that matches everywhere weigh almost nothing even though they verify, and emulation must actually execute non-degenerate code. A reconstruction is grounded only when nothing is refuted and the verified weight reaches --min-information (default 1.0). This follows the CORE refinement of FActScore: credit only claims that are factual, informative and non-repetitive. reverify reconstruct --samples N draws several proposals per round and lets the verifier — not the model's confidence — select among them.

EXAMPLE.md walks through one run on kernel32.dll — the model proposes the textbook prologue from prior, the verifier refutes it with the real bytes, and the model corrects to grounded, with no API key and no specific model. BENCHMARK.md is the reproducible measurement behind the numbers above.

The ledger: state that survives a context reset

Every agent harness handles a full context window the same way — a model summarizes the transcript, the rest is dropped, and the docs warn that repeated compactions degrade accuracy. That loss is unavoidable for free-form conversation, because nothing in a transcript says which parts were state and which were chatter.

Reverify's loop can do better for itself, because it already draws that line: the only things that matter are what the tools verified, observed, proved — and refuted. Everything else (the model's prose, its unverified guesses) was never trusted, so dropping it loses nothing. Since v0.8.0 exactly that state is written to disk as it happens:

• .reverify/ledger/<sha256>.json per binary (content-keyed, so a renamed copy shares its ledger), checkpointed after every round — a crash, a /clear, an auto-compact or a new process all resume from the same grounded position.
• Negative memory: refutations come back as KNOWN FALSE, so a fresh context does not re-propose the same wrong prior — the part a summary usually drops.
• Bounded in context, unbounded on disk: the prompt shows the most recent --max-facts (proof-grade facts pinned), and a deterministic ladder trims the shown fact sheet to --prompt-budget characters (kernel32.dll: 43k chars fit a 20k budget with the section table, entry point and header intact). Scoring uses the full sheet, so hiding a fact never makes restating it profitable, and a claim already in the ledger scores zero (known).
• Lazy hand-off: the hook injects one index line per binary; the facts are pulled on demand, so recovering state costs a few dozen tokens, not a slice of the fresh window.

reverify reconstruct target.exe --goal "..."   # resumes from .reverify/ automatically
reverify ledger target.exe                     # what is established, what is known false
reverify ledger --hook                         # Claude Code SessionStart hook (compact|clear|resume)

Over MCP the same happens with no setup: re_verify_claim records every grounded result, and re_ledger hands them back after the host compacts or clears its context (the server's instructions tell the agent to do so). Nothing unverified is ever stored — claim notes are excluded on purpose.

The semantic layer: functions, calls and cross-references

Bytes, instructions, imports and emulation are what the deterministic core can judge on its own. The claims analysts actually make — function X calls Y, this string is referenced from that routine, this code is reachable from the entry point — need function boundaries and cross-references, which means a real program-analysis engine. Reverify does not build one. It stands on angr (pip install "reverify[angr]") and keeps its own part thin: an engine-neutral view of functions, call edges, data references and reachability, and four claim kinds checked against it.

reverify functions msimg32.dll                                 # what the engine recovered
reverify verify msimg32.dll \
  --claim '{"kind": "calls", "params": {"from": "AlphaBlend", "to": "SetLastError"}}' \
  --claim '{"kind": "references", "params": {"to": 12632, "space": "rva", "from": "AlphaBlend"}}' \
  --claim '{"kind": "function_at", "params": {"offset": 4112, "space": "rva"}}' \
  --claim '{"kind": "reachable_from_entry", "params": {"name": "DllInitialize"}}'

A refuted calls lists the function's real callees and a refuted references lists the functions that do reference the address, so a model can fix the claim instead of guessing again. observe: true reads instead of asserts (a function's size, blocks and callees; the referencing functions of a string).

Honesty about strength: a recovered control-flow graph is analysis-derived — CFGFast is heuristic and can miss or split functions — so semantic verdicts name the engine and are recorded at a DERIVED tier below VERIFIED. Without an engine the pure fallback only knows what is independently certain (the entry point and the exports are function starts) and answers INCONCLUSIVE for everything else, never a guess. And the engine is checked the way the readers are: the export table, parsed independently of angr, must agree with the functions it recovers.

The toolkit

MCP server

Reverify exposes the toolkit to AI agents over the Model Context Protocol:

python reverify/mcp_server.py

Point Claude Code or Cursor at it and the agent can parse, disassemble, and scan binaries directly — with the deterministic tools as ground truth. The re_verify_claim tool exposes the verification loop, so an agent can have its own hypotheses judged against the bytes before it reports them — and records every grounded result in the binary's ledger. re_ledger restores that state after the host's own compaction or /clear (see The ledger); ledgers are also exposed as reverify://ledger/<sha> resources.

Status

v0.9.0 — the semantic layer, on PyPI (pip install reverify). The tool-grounded judge — a claim about the binary is checked against the actual bytes and returned as VERIFIED / REFUTED / INCONCLUSIVE / OBSERVED / INVALIDATED with evidence — ships as reverify verify and the re_verify_claim MCP tool, and reverify reconstruct closes the loop. v0.3.0 brought the mature engines (capstone, unicorn, lief); v0.4.x hardened the loop against gaming (information-weighted scoring measured from the binary, address spaces, typed reads, observe-then-assert, dependencies) and added a testbed that cross-checks the readers themselves (pure parser vs lief on real binaries, disassembler/emulator vs capstone, Unicorn and known-answer vectors, plus fuzzing). v0.5.0 adds the strongest grounding — the behavior_equiv claim runs the original function and a candidate reconstruction over shared inputs and compares outputs, returning a concrete counterexample on a mismatch (the ExeBench / LLM4Decompile re-executability methodology). v0.6.0 makes the reconstruction loop two-stage (observe, then hypothesize) with an established-facts ledger: only what the tools verified or read is carried between rounds, so the model can't build on its own earlier guesses — the defense against context hallucination. v0.7.0 adds a proof tier: the prove_equiv claim uses Z3 to prove two expressions equal for all inputs (verifying MBA deobfuscation), giving an honest strength ladder — proven > tested > observed. v0.8.0 makes the loop's state durable: a per-binary ledger of what the tools verified, observed, proved and refuted, checkpointed every round and restored after /clear, compaction or a restart — lossless by construction, because nothing the model said on its own was ever kept. v0.9.0 adds the semantic layer on angr: function boundaries, the call graph and cross-references as function_at / calls / references / reachable_from_entry claims, recorded at an honest DERIVED tier, with the export table as an independent oracle for the engine. Tested with 208 unit tests, so the verifier is not just trusted, it is checked.

License

MIT — see LICENSE.