Reverify: a deterministic judge for AI claims about binaries

The failure mode reverify is built around

Ask a model to reconstruct a struct or an algorithm from a stripped binary and it will produce offsets, sizes and behaviour with the same tone it uses for a function signature it has actually read. The README states the problem directly: in binary analysis the hallucination problem is worse than in source code, and the question of whether the model just made that up is the single biggest blocker to using AI for real reverse engineering. Reverify's answer is procedural rather than statistical. The model is allowed to propose. It is not allowed to assert. Every structural or behavioural claim is routed to a deterministic tool, which returns VERIFIED, REFUTED or INCONCLUSIVE along with the bytes it observed. Nothing becomes a fact until it survives that step. The audience is narrow on purpose: malware analysts, CTF players and interoperability researchers who already use an agent and already distrust its output. The README also points to reverify equiv for ordinary Python or C, where a candidate implementation and a reference are run over shared inputs and compared, so the same gate applies to an AI-written refactor.

The verification loop and its claim kinds

The unit of work is a claim, expressed as JSON and passed either inline or through --claims-file claims.json. The README gives this example: reverify verify sample.bin --claim '{"kind": "instructions", "offset": 4096, "mnemonics": ["push", "mov", "sub"], "note": "function prologue"}'. A second example checks computation rather than structure, using kind emulate_result with a hex code string, an arch value of x86, and expect_registers set to {"eax": 8}. The documented kinds split into byte-level reads (bytes_at, u16_at, u32_at, u64_at), presence checks (pattern_present, string_present, import_present, export_present, section_present), disassembly (instructions, with mnemonics and optionally operands), execution and equivalence (emulate_result, behavior_equiv, prove_equiv), format-specific dissection (protobuf_field), and a semantic group (function_at, calls, references, reachable_from_entry). Address handling is explicit: offsets are file offsets unless a claim sets "space" to "rva" or "va", in which case the verifier translates through the section table and echoes all three addresses. The CLI exits non-zero if anything is refuted, which is the part that makes the tool usable as a gate rather than a report.

What runs underneath, and what happens without it

The deterministic core is pure Python and covers PE, ELF and Mach-O parsing, x86, x64, ARM and ARM64 disassembly, AOB pattern scanning, CPU emulation, Protobuf and TLV dissection, and Frida hook generation. The README claims it installs clean with no Ghidra, which matters if your analysis host is a locked-down container. Optional engines change the depth of the answers rather than the interface: pip install "reverify[full]" swaps in capstone for disassembly, unicorn for real CPU emulation, lief for the three binary formats and Z3 for proofs, while pip install "reverify[angr]" adds angr for function boundaries, the call graph and cross-references. The fallback behaviour is stated plainly: if an engine is not installed, the toolkit falls back to the pure-Python core, and reverify backends shows what is active. That design keeps the install small but it also means two machines running the same claim can return different verdicts, and the semantic claim kinds are the ones most likely to depend on angr being present. Check reverify backends before comparing results across environments.

Getting it running from PyPI or from a checkout

The documented install is pip install reverify for the core, with the extras noted above for the heavier engines. The quick start then runs reverify auto sample.bin --json, which is the broad sweep, and reverify parse-pe sample.exe --json for format parsing on its own. There is a second path for people who do not want to install anything: python reverify/cli.py auto sample.bin --json, python reverify/cli.py parse-pe sample.exe --json and python reverify/cli.py disasm 90505831C0C3 --arch x86_64 all run from a checkout using the standard library only. That is a real convenience for air-gapped work, and it is also a constraint to understand, because the checkout path cannot use capstone, unicorn, lief or Z3 unless they are installed in the same interpreter. The MCP server is the other entry point, and the README frames it as the reason agents such as Claude Code and Cursor can call the tools directly rather than shelling out. For an agent integration, the MCP route is the one to evaluate first, since it removes the need to parse CLI output back into the model's context.

The benchmark claim and how to read it

The headline number is specific enough to be checkable. On 71 real Windows system files, the README says the AI's textbook answer was wrong 97% of the time, that reverify caught every one, and that it never accepted a wrong claim (0 of 71). The same gate is described as running in CI on Linux and macOS on every push, with an independent aarch64 run finding the same result. The supporting files are EXAMPLE.md and BENCHMARK.md, and the script is python benchmarks/prologue_prior.py. Two things are worth separating. The 97% figure is a property of the model's prior on function prologues, not of reverify. The 0 of 71 figure is the one that describes the tool, and it is a soundness claim: no wrong claim was accepted. The README does not present a completeness figure in the material available here, which is the natural next question, because a verifier that returns INCONCLUSIVE on everything would also score 0 of 71. The release notes for v0.10.0 mention a confusion matrix and a reproducible corpus, so the false-negative side may be documented in BENCHMARK.md. Read it there rather than assuming.

Rollover, and why it is a separate feature

The second capability has nothing to do with binaries. reverify rollover hands a session off to a file and starts a fresh one, instead of letting the agent auto-summarise its own context. The README's framing is that long tasks drift or require /clear, and that a lossy summary is the wrong primitive for preserving grounded facts. The release notes for v0.11.0 describe the same feature as lossless context rollover across Claude Code, Codex, Gemini CLI and OpenCode. Note the coupling: this is the mechanism that lets verified facts survive a reset, so the two features are not as unrelated as they first appear. If your workflow is a long analysis session where the agent accumulates verified offsets and function boundaries, rollover is what keeps those from being paraphrased away. If your sessions are short, it is dead weight. The README does not describe the handoff file format or how conflicts between the old and new session are resolved, so treat that as something to inspect in the repository before depending on it.

Where the approach breaks down

The gate is only as strong as the claim language. A model that phrases a wrong idea as something outside the documented kinds, or that reports a conclusion without emitting a claim at all, produces no refutation and no non-zero exit. The tool constrains what is checked, not what the model says to the user. There is a second limit in the fallback path: without angr, function boundaries, the call graph and cross-references are unavailable, so function_at, calls, references and reachable_from_entry lose their backing, and without unicorn the emulate_result and equivalence kinds are weaker than they read. Offsets are another place to be careful. The default is a file offset, and a claim written against an RVA without "space": "rva" will be checked against the wrong bytes, which is a silent mistake rather than an error. Finally, this is not a decompiler and does not claim to be one. It verifies statements; it does not reconstruct a program for you, and it will not tell you what a function is for. If you want readable pseudocode, reverify is the wrong layer.

How it differs from Ghidra and from plain unit tests

The obvious comparison is Ghidra, and the README makes the contrast itself by noting the core installs with no Ghidra. The difference is in what each produces. Ghidra gives a human an interactive decompiler and a scripting API; the analyst reads the output and decides what is true. Reverify gives an agent a set of checkable predicates and a verdict, and the analyst reads VERIFIED or REFUTED with the observed bytes attached. Ghidra is better at exploration and at producing something a person can read. Reverify is better at stopping an agent from writing a wrong offset into a report, and it runs headless in CI where a GUI decompiler does not fit. The second comparison is to ordinary tests. For the equiv path, running a candidate against a reference over shared inputs is close to property-based testing, and the difference is that a refutation comes back with the input and both outputs, so the failure is immediately actionable. The cost is that you have to supply a reference implementation, which is exactly the thing you may not have when you are reversing a binary in the first place.

Maintenance cost and licence

The project is MIT licensed and not archived, with the last push recorded as 2026-09-07 and three releases in the days before it: v0.11.0 for rollover, v0.10.0 for the evidence and benchmark work, and v0.9.1 for an ARM64 routing fix and soundness without the engines. That cadence is fast, and the v0.9.1 note is a useful signal about the fallback path being treated as a first-class configuration rather than an afterthought. The upgrade cost depends on which extras you install. The pure-Python core has no compiled dependencies, so upgrading is a pip install away. The full and angr extras pull in capstone, unicorn, lief, Z3 and angr, and a change in any of those can alter a verdict without any change in reverify itself, which is why reverify backends should be part of whatever record you keep alongside a result. MIT places few obligations on redistribution, but the optional engines carry their own licences, and the README does not enumerate them. Check each one if you ship a bundled environment. This is not legal advice.

Editorial conclusion

Adopt reverify if your agent already makes structural claims about PE, ELF or Mach-O files and you want a non-zero exit code when one of them is wrong, or if you need a session handoff that does not summarise. Do not adopt it as a substitute for a decompiler, as a source-code static analyser, or if you cannot install capstone, unicorn, lief and Z3 and still expect the semantic claim kinds to work. Before trusting a number, run python benchmarks/prologue_prior.py yourself and read BENCHMARK.md to confirm what corpus the 71 files come from and which backends were active for the run.

Official sources

1. 2akouwu/reverify on GitHub
2. Issues
3. License: MIT
4. README
5. Releases