Reverify

What is Reverify about?

Reverify pairs large language models with a pure‑Python reverse‑engineering toolkit that acts as an impartial judge. The model proposes a claim (e.g., a struct offset, a disassembly sequence, or an algorithmic behavior) and the toolkit checks the claim against the real bytes, returning VERIFIED, REFUTED, or INCONCLUSIVE with verifiable evidence.

How to use Reverify?

1. Install the core CLI (and optional engines) via PyPI:

   pip install reverify            # pure‑Python core
   pip install "reverify[full]"   # adds capstone, unicorn, lief, Z3
   pip install "reverify[angr]"   # adds angr for semantic analysis
   

2. Run the MCP server (if agents need remote access):

   python -m reverify.mcp_server
   

3. Verify a claim directly from the CLI:

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

4. Automate a reconstruction loop where an AI proposes, the tools verify, and the loop iterates until grounded:

   reverify reconstruct target.exe --goal "map loader, list imports, enumerate exports"
   

5. Persist state across resets with the ledger (.reverify/ledger/<sha>.json) and use reverify rollover to hook into CLI agents such as Claude Code, Codex, Gemini, or OpenCode.

Key Features

• Deterministic verification core – PE/ELF/Mach‑O parsing, x86/x64/ARM disassembly, AOB scanning, CPU emulation, protobuf/TLV decoding, Frida hook generation, all in pure Python.
• Optional high‑performance back‑ends – capstone, unicorn, lief, Z3, and angr can be added without changing the CLI.
• Claim language – supports byte reads, typed reads, pattern presence, string presence, instruction sequences, emulation results, behavioral equivalence, proof‑based equivalence, protobuf fields, imports/exports, sections, and semantic claims (function_at, calls, references, reachable_from_entry).
• Evidence‑backed results – each verdict includes the binary SHA‑256, tool versions, and concrete evidence (observed bytes, counter‑examples, proof logs).
• Information‑weighted scoring – verified claims contribute only if they provide non‑trivial information, preventing cheap “always true” assertions.
• Ledger for persistence – verified, observed, proved, and refuted facts are checkpointed per binary, surviving /clear or context compaction.
• Rollover & orchestration – integrates with agent CLIs to automatically hand off a compact fact sheet and ledger when context windows fill, keeping long tasks reliable.
• MCP server – exposes the verification loop (re_verify_claim) and ledger (re_ledger) to any Model Context Protocol‑compatible agent.

Use Cases

• Malware analysis – guarantee that AI‑generated disassembly or deobfuscation claims match the actual malicious binary.
• CTF reverse‑engineering challenges – automate hypothesis testing without manual verification.
• Software interoperability – validate that regenerated source‑level structures or algorithms faithfully reproduce binary behavior.
• Secure AI‑assisted development – ensure AI‑suggested code changes are functionally equivalent to the original implementation.
• Research on hallucination mitigation – benchmark LLMs on binary RE tasks with a ground‑truth verification harness.

FAQ

Q: Do I need to install heavy dependencies? A: No. The core works with only the Python standard library. Optional back‑ends (capstone, unicorn, lief, Z3, angr) can be added via extra install tags.

Q: How does Reverify handle wrong claims? A: Refuted claims are reported with the observed value and are recorded as KNOWN FALSE in the ledger, preventing the model from re‑proposing the same error.

Q: Can I verify source‑code transformations? A: Yes. The reverify equiv command runs a reference implementation and a candidate on identical inputs and reports mismatches.

Q: Is the MCP server secure for private binaries? A: The server runs locally and does not transmit binaries. It is intended for authorized reverse engineering only (see SECURITY.md).

Q: What happens if I run without optional engines? A: The verifier falls back to the pure‑Python implementations, providing deterministic but less detailed analysis (e.g., no full CFG from angr).

Q: How is the ledger stored? A: As JSON files under .reverify/ledger/<sha256>.json. Each entry records the claim, verdict, evidence, and engine tier (VERIFIED, DERIVED, etc.).

AI is confident and often wrong: it invents an API, a struct field, an offset, or what a function does, and says it like fact. Reverify makes a deterministic tool the judge — the model proposes a claim, the tool checks it against the actual artifact, and it comes back VERIFIED / REFUTED with evidence. The model never gets to assert a fact on its own.

Two things it does today:

• Keeps your AI honest — every structural or behavioral claim is checked against ground truth, not trusted, and only what survives becomes a fact (reverify verify, or the MCP server your agent already talks to).
• Keeps your AI's context from rotting — instead of a lossy auto-summary, reverify rollover hands the session off to a file and starts a fresh one, so long tasks don't drift or need /clear. Works in Claude Code, Codex, Gemini CLI and OpenCode.

The hardest place to prove the first point is binary reverse engineering, where hallucination is worst — so that's where the numbers come from. On 71 real Windows system files the AI's textbook answer was wrong 97% of the time; reverify caught every one and never accepted a wrong claim (0 of 71; the same gate runs in CI on Linux and macOS every push, and an independent aarch64 run found the same) (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.
• Not only binaries — reverify equiv <reference> <candidate> --lang python (or C) runs a candidate implementation and a reference over shared inputs and checks they agree, so an AI's rewrite or refactor is tested, not trusted — a refutation comes back with the input and both outputs. The same rigour, aimed at ordinary source code.
• 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.

Evidence, not claims

Everything above is checkable without trusting the author:

• The verifier is checked by independent judges, not by its own tests: the pure parser against lief on real binaries, the disassembler against capstone, binutils objdump and hand-verified Intel vectors, the emulator against Unicorn, the semantic engine against the export table — plus fuzzing that a malformed file never crashes the reader and that a wrong claim is never VERIFIED. All of it runs in CI on Linux, Windows and macOS, with and without the engines; a nightly job fuzzes 20k inputs.
• The benchmark runs in CI on every push, on each platform's own system binaries, and fails the build if a single wrong claim is VERIFIED. Each run leaves a machine-readable record — SHA-256 of every binary, verdicts, tool versions — as an artifact; reference runs live in benchmarks/results/, and a third-party aarch64 replication is in BENCHMARK.md.
• The verifier is measured like a classifier: for every claim kind, known-true and known-false claims on real binaries give a confusion matrix — 0 false VERIFIED of 475 known-false claims, 0 known-true claims missed — gated in every CI job.
• Every verdict carries a receipt: reverify verify --json (and re_verify_claim) include the binary's SHA-256, the reverify version and which engines judged, so a report can be handed over and replayed rather than believed. Releases ship with a SLSA build provenance attestation.
• A replication package: benchmarks/README.md — one command per benchmark, a pinned Dockerfile, expected output, and how to submit a run; a model-in-the-loop benchmark anyone can run against any OpenAI-compatible endpoint.

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 loop that never fills up: fresh sessions with a verified hand-off

For a long task the ledger is not enough on its own — something has to decide when to drop the transcript and what the next context starts with. reverify orchestrate runs a goal as a sequence of fresh-context sessions and keeps the model in charge of the timing:

reverify orchestrate target.exe --goal "map the loader: entry, imports it really uses, exports" \
  --driver claude           # Claude Agent SDK on your Claude Code login; or openai (OPENAI_* env), or mock

• The model works through a small JSON protocol: propose claims, take notes, update its hand-off, ask for a rollover when its context feels long or confused, or declare done.
• A rollover also happens on a token budget per session and on drift — when restatements (trivial, echo, already-known) dominate the last turns, the loop is going in circles and gets a fresh start.
• The next session opens with the fact sheet, a one-line ledger index and a bounded hand-off. ESTABLISHED and KNOWN FALSE come from the ledger, never from the model; the model's own decisions and notes travel labelled unverified. That is the difference from every "summarize and continue" loop: a hallucination cannot ride the hand-off into the next context as if it were a fact.
• The checkpoint (.reverify/sessions/<task>/checkpoint.json, with a history) resumes across runs (--task <id>). Over MCP, re_checkpoint saves and loads the same hand-off so an agent that lives in someone else's context (Claude Code, Cursor) can do the same before its host compacts or clears.

A real run with the Claude Agent SDK driver on msimg32.dll (2 sessions × 4 turns, no API key): 15 grounded facts across the rollover — the real entry-point instructions, the machine type, header pointers read through typed observes — 2 guessed call-stub patterns refuted, 0 false accepts, and the second session started from the ledger, not from a summary (benchmarks/results/orchestrate-claude-msimg32-2026-09-04.json).

Any agent CLI without compaction: reverify rollover

The same rule applied to an interactive session — Claude Code, Codex CLI, Gemini CLI or OpenCode. Built-in compaction is turned off; the model hands off to files, and instead of a model-written summary the session is replaced wherever the CLI lets a hook do that (Gemini CLI, OpenCode) or a launcher owns the process. Where it does not (a plain claude or codex), reverify keeps the context lean rather than pretending to clear it: bulky tool output goes to files that stay re-readable, edits stay local, exploration goes to subagents, and the hand-off is always current. We are asking those vendors for the missing primitive.

pip install reverify
reverify rollover install          # every CLI found on PATH (or --harness claude,codex,gemini,opencode); backups kept
reverify rollover doctor           # what is wired, whether the hook commands still resolve, recent events

Then use your CLI exactly as before. The hooks do the hand-off; Gemini CLI and OpenCode also open the fresh session themselves. For Claude Code and Codex, or whenever you want the fresh session to open automatically, start the CLI through the launcher instead:

reverify rollover claude                    # same arguments as the CLI itself, e.g.
reverify rollover codex --full-auto
reverify rollover instructions --write AGENTS.md   # optional: the protocol paragraph for the model

• A session nobody can end keeps growing — check doctor. The hooks can write the hand-off but cannot end a Claude Code or Codex session. If you start the CLI yourself, or through the desktop app, a background job (claude --bg), or Remote Control server mode, the hand-off is written and nothing follows it: with native compaction off the conversation has no ceiling (one measured session reached 909k tokens before its owner noticed). reverify rollover doctor now reports receipts that no launcher consumed. Either start the CLI through the launcher (reverify rollover claude --remote-control keeps phone/web access through Remote Control), or set REVERIFY_ROLLOVER_SUCCESSOR=bg in ~/.claude/settings.json → env: every receipt then starts a fresh claude --bg session that opens with the hand-off and appears in your session list, and you switch to it. Neither route resumes or rewrites the old transcript. The successor starts in the old session's project directory (Claude Code keys trust and MCP approvals per project), and doctor names a successor that is stuck waiting on an approval.
• Small windows stay safe. Native compaction is off, so when the harness records the model's context window (Codex does) the threshold is capped at 75% of it and the hand-off is refreshed more often.
• Guard. At the harness's "turn finished" hook (Claude Code / Codex Stop, Gemini AfterAgent, OpenCode session.idle via a plugin) the guard measures the live context from the harness's own transcript. At the threshold (REVERIFY_ROLLOVER_TOKENS, default 200k), or when the model itself runs reverify rollover request --reason ..., it blocks one stop and asks the model to write the hand-off file — fixed sections, labelled UNVERIFIED — and its memory index. Nothing is summarized in the conversation.
• Receipt, fail closed. On the next stop the guard checks that the hand-off was really rewritten and is well-formed; only then does it write a receipt carrying the transcript's SHA-256 and the user's verbatim first and latest messages. A missing or malformed hand-off means no receipt and a re-arm 100k further up.
• Fresh session. Whoever can end the session does it: the launcher for any CLI (waits for the receipt, gives a queued user message a moment to land — if one did, that rollover is off — ends the session, starts a fresh one whose first message points at the hand-off and quotes the original request verbatim); Gemini CLI in-process through its own clearContext, with the opening injected on the next turn; OpenCode through the SDK (new session, opening prompt). The old transcript stays on disk as an audit trail and is never resumed; every decision is appended to ~/.reverify/rollover/events.jsonl.
• What install touches, all with backups and reversible by uninstall: Claude Code ~/.claude/settings.json (hooks, autoCompactEnabled: false); Codex ~/.codex/hooks.json
  • config.toml ([features] hooks = true, a compaction limit no session reaches); Gemini ~/.gemini/settings.json (hooks, model.compressionThreshold above 1); OpenCode ~/.config/opencode/plugins/reverify-rollover.js + opencode.json (compaction.auto: false).

Compare with a compaction summary: the hand-off is written while the model still has the whole context, into a file with a fixed shape, separated from verified facts (memory files, the ledger) — and the conversation that produced it is dropped, not paraphrased. Zero dependencies; the hooks fail open, the rollover fails closed.

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

Command	What it does
reconstruct	Closed loop: a model proposes claims, the tools verify, iterate until grounded
verify	Check a claim about the binary against the tools — VERIFIED / REFUTED / INCONCLUSIVE
verify (behavior_equiv)	Run the original function and a candidate over shared inputs; a mismatch returns a counterexample
auto	Auto-triage: detect format, architecture, sections, top strings
parse	PE / ELF / Mach-O: arch, entry, sections, imports, exports (lief when installed)
parse-pe	PE32/PE32+ headers, imports, exports
backends	Show which engines are active (capstone / unicorn / lief)
disasm	x86/x64 disassembly of hex or a section
pattern-scan	AOB scan with ?? wildcards
strings	ASCII + UTF-16LE extraction with offsets
emulate	CPU register/stack micro-emulation
decode-protobuf / decode-tlv	schema-less wire-format dissection
gen-hook	Frida interceptor script generation
hexdump	aligned hex dump
diff-patch	binary diff / patch generation
audit-boundary	defensive filesystem/SSRF boundary audit

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.

Community

Shared on LINUX DO. Bugs and false-accept reports: open an issue.

License

MIT — see LICENSE.