TL;DR

Reverify is a Python CLI and MCP server built on one rule: the model proposes, a deterministic tool decides. An LLM can hypothesize anything it likes about an artifact — a function prologue, an imported symbol, whether a refactor is behavior-equivalent — but nothing counts as a fact until a tool checks it against ground truth and returns VERIFIED or REFUTED with evidence. The model never gets to assert a fact on its own.

It picked the hardest place to prove that idea: binary reverse engineering, where hallucination is at its worst. On 71 real Windows system DLLs, the model’s “textbook” answer for the entry-point prologue was wrong 97% of the time; Reverify’s verifier refuted every wrong claim and accepted zero. That gate now runs in CI on Linux, macOS, and Windows on every push and fails the build if a single wrong claim is ever marked VERIFIED.

Key facts as of September 9, 2026:

  • 1,053 GitHub stars, 217 forks, created August 31, 2026 — nine days old
  • MIT licensed, pip install reverify, pure standard library with zero required dependencies; optional capstone / unicorn / lief / Z3 / angr engines upgrade it in place
  • Ships as an MCP server (re_verify_claim, re_ledger, re_checkpoint, …) for Claude Code, Cursor, and any MCP client
  • reverify rollover replaces auto-compaction in Claude Code, Codex CLI, Gemini CLI, and OpenCode with a file-based hand-off
  • 0 false VERIFIED across 275 binaries in four formats/architectures; v0.8.0 → v0.11.0 shipped September 3–4, 2026

This is a narrow tool with a very general idea inside it. If you do binary analysis, malware triage, or CTF work with an AI agent, it is immediately useful. If you don’t, the interesting part is the architecture — an anti-hallucination pattern most agent frameworks still don’t implement.

The problem Reverify is built around

Every agent framework has the same soft spot: the model’s own output goes back into its context as if it were true. It guesses an API signature in turn 3, builds on it in turn 8, and by turn 20 an entire plan rests on something nobody checked. When the window fills, a summarizer compresses the transcript — and the guess and the verified fact get the same treatment, because nothing in a transcript marks which is which. Reverify’s author frames it for binaries: “Ask a model to reconstruct a struct or an algorithm from a binary and it will confidently invent offsets, sizes, and behavior.”

The fix separates two roles most agents blur. The proposer — the LLM — emits claims: structured JSON hypotheses about the artifact. The judge — deterministic tooling — checks each claim against the actual bytes and hands back a verdict plus the evidence it saw. Only verified claims become facts. Refuted claims come back with what the tool observed, so the model can correct instead of re-guessing.

The verification loop in practice

pip install reverify              # pure-Python core
# or: pip install "reverify[full]"  → capstone + unicorn + lief + z3
reverify auto sample.bin --json   # triage: format, arch, sections, strings
reverify backends                 # which engines are active

A claim is a JSON object with a kind and whatever the verifier needs to check it:

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

The verifier disassembles at that offset and answers VERIFIED, REFUTED, or INCONCLUSIVE. Claims batch from a file (--claims-file claims.json), and the CLI exits non-zero if anything is refuted, which makes it a drop-in CI gate.

The claim vocabulary is wider than it first looks. Structural kinds: bytes_at, typed reads (u32_at / u64_at), pattern_present, string_present, import_present, export_present, section_present. Behavioral kinds: emulate_result (run the bytes, compare registers), behavior_equiv (run the original function and a candidate reconstruction over shared inputs), and prove_equiv (Z3 proves two expressions equal for all inputs — the tool for MBA deobfuscation). The v0.9.0 semantic layer adds function_at, calls, references, and reachable_from_entry on top of angr. A refuted bytes_at even reports where the expected bytes actually are, and "observe": true lets the model read a value instead of guessing it.

A real hallucination, caught

The repository’s EXAMPLE.md walks through one run on C:\Windows\System32\kernel32.dll with Claude as the proposer. The model saw only a fact sheet — format, architecture, sections, imports, strings, entry RVA — and not the entry-point disassembly.

Round 1, the model proposed from priors:

[REFUTED ] instructions @ entry (rva 0x2c500)  mnemonics ["push","mov","sub"]
           note: "DllMainCRTStartup: standard frame prologue (prior guess)"
[VERIFIED] export_present  CreateFileW
[VERIFIED] export_present  GetProcAddress
[VERIFIED] section_present .text

The textbook push rbp; mov rbp, rsp; sub rsp, N frame prologue is the strongest prior in any model’s training data. It is wrong here. The verifier refuted it and returned the real bytes — the MSVC x64 shadow-space prologue:

mov qword ptr [rsp + 8], rbx ; push rdi ; sub rsp, 0x20 ; mov edi, edx ; mov rbx, rcx

Round 2, the model corrected from evidence:

[VERIFIED] instructions @ entry  mnemonics ["mov","push","sub","mov","mov"]
           operands ["qword ptr [rsp + 8], rbx","rdi","rsp, 0x20","edi, edx","rbx, rcx"]  mode=exact
Verified 3/3.  Information 1.236.  Trustworthy: True  Grounded: True

That Information 1.236 line is the second clever piece. “Every claim verified” is trivially reachable — assert that the file starts with MZ and that .text exists. So Reverify weighs each verified claim by how much it actually says: restating the fact sheet weighs zero, and the rest is scored by how rare and high-entropy the expected content is in this specific binary. A reconstruction is only “grounded” when nothing is refuted and the verified weight clears --min-information (default 1.0).

The benchmark: 275 binaries, 0 false accepts

BENCHMARK.md applies the textbook-prologue prior blind to a deterministic sample of the host’s own system binaries and records, per file, whether the prior was wrong and whether the verifier ever accepted a wrong claim.

PlatformFormatTestedPrior wrongFalse VERIFIED95% upper bound
Windows 11 (reference run)PE x86 + x86_647169 (97%)05.1%
Linux x86_64 (ubuntu-latest)ELF404008.8%
macOS (macos-latest, x86_64 slice)Mach-O777704.8%
Windows Server (windows-latest)PE686805.3%

Pooled with a third-party aarch64 replication: 275 binaries, 4 formats/architectures, 0 false VERIFIED, with a pooled 95% Wilson upper bound of about 1.4% on the false-accept rate. Two of the 71 Windows DLLs genuinely open with push; mov and were correctly verified — the benchmark is not rigged to always refute.

A control corpus makes this more credible: CI compiles two small C libraries with gcc, clang, and MSVC at -O0 and -O2. At -O0 the frame-pointer prologue really is there and verifies; at -O2 it isn’t and gets refuted. Every run leaves a record with the SHA-256 of every binary and every verdict under benchmarks/results/, and releases ship with SLSA build provenance. For a nine-day-old solo project, this is an unusual amount of evidence engineering.

The ledger: facts that survive /clear

The second half of the project generalizes from “verify a claim” to “manage context.” Every harness handles a full window the same way: summarize and drop the rest. Reverify’s argument is that this loss is only unavoidable because the transcript doesn’t know which parts were state. Its loop does know: the only things that matter are what the tools verified, observed, proved, and refuted. Everything else was never trusted, so dropping it loses nothing.

Since v0.8.0 that state lives in .reverify/ledger/<sha256>.json per binary (content-keyed, so a renamed copy shares its ledger), checkpointed after every round. Refutations are stored as KNOWN FALSE, so a fresh context doesn’t re-propose the same wrong prior — the part a summary usually drops.

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

Over MCP, re_verify_claim records every grounded result and re_ledger hands them back after the host compacts or clears. re_checkpoint notes are explicitly labelled UNVERIFIED — “only re_verify_claim results become facts.”

reverify orchestrate closes the loop across sessions, running a goal as a sequence of fresh contexts and rolling over on the model’s request, a token budget, or drift. The recorded run on msimg32.dll with the Claude Agent SDK driver — 2 sessions × 4 turns — produced 15 grounded facts across the rollover, 2 refuted guesses, 0 false accepts, and a second session that started from the ledger rather than a summary.

reverify rollover: the same idea for any agent CLI

This is the piece most readers will actually try, because it has nothing to do with binaries.

reverify rollover install          # wires hooks into every CLI on PATH (backups kept)
reverify rollover doctor           # what is wired, recent events
reverify rollover claude           # launch Claude Code through the launcher
reverify rollover codex --full-auto

install turns off native auto-compaction in each CLI and installs a guard at its “turn finished” hook. At the threshold — REVERIFY_ROLLOVER_TOKENS, default 200k — or when the model runs reverify rollover request, the guard blocks one stop and asks the model to write a hand-off file with fixed sections, labelled UNVERIFIED. Nothing is summarized inside the conversation.

The design is fail-closed: on the next stop the guard checks that the hand-off was really rewritten, and only then writes a receipt carrying the transcript’s SHA-256 and the user’s verbatim first and latest messages. Then whoever can end the session does it — the launcher for any CLI, Gemini in-process, OpenCode via the SDK. The old transcript stays on disk as an audit trail. In the author’s words, the hand-off is written while the model still has the whole context, “and the conversation that produced it is dropped, not paraphrased.”

The same rule now reaches ordinary code: reverify equiv <reference> <candidate> --lang python (or C) runs both implementations over shared inputs and returns a counterexample on mismatch, so an AI’s refactor is tested, not trusted. It is a small feature today, but it is the one that could pull Reverify out of its niche.

Setting it up as an MCP server

{
  "mcpServers": {
    "reverify": {
      "command": "python",
      "args": ["/path/to/reverify/reverify/mcp_server.py"]
    }
  }
}

Exposed tools: re_auto_triage, re_parse, re_pattern_scan, re_disasm, re_verify_claim, re_semantic, re_checkpoint, and re_ledger. Once wired, your agent can have its hypotheses judged against the bytes before it reports them, and its grounded facts come back automatically after a /clear.

Community and early feedback

Reverify has not had a Hacker News or Reddit moment yet; the README notes it was shared on LINUX DO, a Chinese-language developer community. The 217-fork-to-1,053-star ratio is unusually high, which usually means people are pulling the code to run the benchmark locally — consistent with a project whose whole pitch is “replicate it yourself.”

The most substantive external feedback is from contributor IMGillusion, who has landed five PRs (ARM64 disassembler routing, an ExeBench adapter, a multi-prior scorecard, among others). Their open issue #14 is the most honest picture of where the loop still breaks:

“When the orchestrate goal is phrased as an open-ended description, the model stops using the structured claim kinds and degrades to raw bytes_at guessing. The run never converges.”

Their repro on a qwen3.8-27b endpoint: /usr/bin/ls with the goal “find the dynamic import list” converged on 14 import_present claims; /usr/bin/cat with an open-ended phrasing of the same goal produced zero structured claims and stalled. The root cause is a prompt gap, and the one-line fix in PR #19 flips the run to 100% structured claims. The verifier is airtight, but the proposer is still a language model, and small prompt details decide whether the loop converges.

Honest limitations

  1. Nine days old, single-author, alpha. 74 of 82 commits are from 2akouwu; PyPI’s classifier says Development Status :: 3 - Alpha. Four versions shipped in 48 hours, and PyPI currently lists 0.10.0 while the repo is at 0.11.0 — APIs will move.
  2. The benchmark measures one prior. The 97%-wrong figure is for the textbook-prologue guess specifically, not a general hallucination rate — the author says to “treat it as a data point, not a headline.”
  3. The pure-Python core is limited. Without capstone/unicorn/lief, semantic claims answer INCONCLUSIVE for almost everything. Real work wants reverify[full]; the semantic layer wants angr, a heavy install, and its verdicts sit at a lower DERIVED tier because CFGFast is heuristic.
  4. rollover has a sharp edge. The hooks can write the hand-off but cannot end a Claude Code or Codex session. Start the CLI yourself with native compaction now disabled and the conversation has no ceiling — the README admits “one measured session reached 909k tokens before its owner noticed.” Use the launcher, set REVERIFY_ROLLOVER_SUCCESSOR=bg, or run doctor regularly.
  5. Authorized use only. Malware analysis, CTF, interoperability research, and software you own — a policy line, not a technical control.

How it compares

ToolWhat it doesJudge is deterministic?Survives context reset?
ReverifyModel proposes claims about bytes/code; tools verify with evidenceYesYes (content-keyed ledger + rollover)
Ghidra / IDA + LLM pluginsLLM annotates a decompilationNoNo
Guardrails / LLM-as-judgeA second model scores the first model’s outputNoNo
Native auto-compaction (Claude Code, Codex)Summarize transcript when fullNoLossy (summary includes guesses)
ExeBench-style re-executabilityCompile and run candidate vs. referenceYesN/A (one-shot)

The unique seat is the combination: deterministic verdicts and a memory that only stores what was verified.

FAQ

Is Reverify free?

Yes. MIT license, pip install reverify, zero required dependencies. The optional engines (capstone, unicorn, lief, Z3, angr) are open-source too.

Does it need an API key or a specific model?

No. The proposer is whatever agent you already run over MCP. reverify orchestrate --driver claude uses your Claude Code login via the Claude Agent SDK; --driver openai takes OPENAI_* env vars for any OpenAI-compatible endpoint; --driver mock runs the loop with no model at all.

How is this different from an LLM-as-judge guardrail?

The judge is not a model. A claim is checked by disassembling, emulating, or proving against the actual artifact, and the verdict comes with the observed bytes. The verifier is itself cross-checked against capstone, Unicorn, lief, and objdump, fuzzed nightly, and gated so that 0 of 475 known-false claims may ever be accepted.

Can I use it on source code, not binaries?

Partially — reverify equiv covers Python and C behavior equivalence. The structural claim vocabulary (bytes_at, import_present, etc.) is binary-specific.

Bottom line

Reverify is two products in one repo. The first is a rigorous reverse-engineering companion for AI agents — if you do binary analysis with Claude Code or Cursor, install it today. The second is a working prototype of an idea the whole agent ecosystem needs: an agent’s memory should contain only what a deterministic tool confirmed, and a context reset should drop the chatter, not the facts.

It is early, niche, and moving fast. But the evidence discipline — receipts on every verdict, a CI benchmark that fails on a single false accept — is better than most tools ten times its age. Watch reverify equiv and reverify rollover; those are the parts that could matter to everyone.

Install: pip install "reverify[full]". Source, benchmarks, and replication package at github.com/2akouwu/reverify.

Sources