Reverify
Stop your AI from making things up.
It proposes; deterministic tools check every claim against ground truth, and only what's verified counts.
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.
"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;
the directory follows OPENCODE_CONFIG_DIR / XDG_CONFIG_HOME exactly as opencode does).
Compare with a compactio
Reverify 是一个防止 AI 智能体编造事实的工具：它用一套确定性工具把模型做出的每一条论断都对照真值加以验证，并以逆向工程作为主要的试验场。