Reverify

A verification layer for coding agents working on binaries: a Python package with a CLI and an MCP server. Its own description is the clearest account of the idea — “it proposes, deterministic tools decide, every claim checked against ground truth with evidence”. A model proposes a claim; the tools check it against the actual bytes and answer VERIFIED, REFUTED or INCONCLUSIVE with the evidence they read. In the repository that deterministic half is code: verifier.py holds the claim kinds and the verdicts, binary.py and pe_parser.py parse PE, ELF and Mach-O, disasm.py disassembles, emulator.py emulates, behavior.py runs a reconstruction beside the original, semantic.py stands on angr, and backends.py reports the active engines. Install the pure-Python core with pip install reverify, add capstone, unicorn, lief and Z3 with pip install "reverify[full]", and angr with pip install "reverify[angr]"; then check a claim with reverify verify, triage a file with reverify auto sample.bin --json, or serve the MCP server with python reverify/mcp_server.py.

Who built itThe account that owns the repository wrote 74 of its 83 commits, 89% of the total; one outside contributor, IMGillusion, wrote five and dependabot three, with one commit carrying no linked account. Seventy-four commits carry a co-author trailer, and 71 of those name a Claude model — Fable 5.1 on 47, Opus 4.8 on 21, Sonnet 5 on 3.

1. 01

   Six days, eighty-three commits, fifteen releases

   The repository was created on 2026-08-31. Its first commit — “Reverify v0.0.0 - verified reverse-engineering toolkit” — landed on 2026-09-02, and its last on 2026-09-07: a change pinning CI dependency versions, reviewed as pull request 18. All 83 commits fall inside September 2026 and all 15 releases fall inside three days, from v0.1.0 (“verification core”) at 14:15 on 2026-09-02 to v0.11.0 (“lossless context rollover across Claude Code, Codex, Gemini CLI, OpenCode”) at 18:13 on 2026-09-04; a v0.0.0 tag exists with no release behind it. The commit signature is the part worth reading. The owner’s account wrote 74 of the 83; the outside contributor IMGillusion wrote five, dependabot three, and one commit has no linked account. Seventy-four commits carry a co-author trailer, 71 of them naming a Claude model — Fable 5.1 on 47, Opus 4.8 on 21 and Sonnet 5 on 3. Nothing has been pushed since 2026-09-07, and the repository stands at 1,252 stars and 237 forks.

2. 02

   The claim is the unit of work, and the tools are the judge

   reverify verify takes a claim about a binary and returns VERIFIED, REFUTED or INCONCLUSIVE with the bytes the tools actually read; the claim is JSON, --claims-file batches them, a claim can declare depends_on so a refuted root invalidates what was built on it, and the command exits non-zero if anything is refuted, so a CI job can gate on a grounded reconstruction. The kinds map onto the deterministic core: typed reads (u16_at, u32_at, u64_at), pattern_present, string_present, instructions, emulate_result, behavior_equiv (run the original and a candidate over shared inputs), prove_equiv (Z3, for all inputs), protobuf_field, import_present, export_present, section_present, and the angr-backed function_at, calls, references and reachable_from_entry. Success is not “everything verified”: the README calls that condition trivially reachable — assert that the file starts with MZ and that .text exists — so each result carries a weight measured from the binary itself, zero for restatements, duplicates and echoes of the tools’ own output, and a reconstruction counts as grounded only when nothing is refuted and the verified weight reaches --min-information. reverify reconstruct --samples N draws several proposals per round and lets the verifier, not the model’s confidence, choose among them.

3. 03

   The proving ground the author chose: reverse engineering

   Where the numbers come from is the author’s own framing, not an outside judgement: the README says binary reverse engineering is “the hardest place to prove the first point ... so that’s where the numbers come from”, and the repository’s one-line description ends with “Reverse engineering is the proving ground.” The probe applies a fixed model prior blind — “a language model asked what a function’s entry prologue looks like tends to answer the textbook frame-pointer prologue push rbp ; mov rbp, rsp” — and only the verifier judges it. On 71 real Windows system files the prior was wrong 69 times, 97%, and the verifier marked 0 wrong claims VERIFIED; the same gate runs in CI on Linux, Windows and macOS on every push, “and fails the build if a single wrong claim is VERIFIED”. Those three runner datasets were wrong 40 of 40, 77 of 77 and 68 of 68, with zero false accepts, and pooled with the reference run and a contributor’s aarch64 run they come to 275 binaries across four formats, 0 false VERIFIED. The benchmark document is explicit about what that means — “0/71 means the rate is below about 5% with 95% confidence, not that it is zero” — and that this prior is one probe at entry points rather than a survey.

4. 04

   A test suite that also checks the checkers

   The project’s claim is that a deterministic tool can settle these questions, so the test layout is part of the argument. Of the 109 files in the tree, 29 are tests — 244 KB against the 436 KB of the package they cover, about 36% of the Python by size — and the largest of them, test_rollover_harness.py at 42 KB, mirrors the largest source file in the repository, rollover_harness.py at 97 KB. verifier.py, the judge itself, is the biggest single module at 60 KB. The suite is not the only check: CONTRIBUTING asks for “a test that would fail without it” and prefers “a differential or known-answer test over a hand-written expectation” for anything touching a reader, and the README says the readers are 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 vectors, the emulator against Unicorn, the semantic engine against the export table — with CI running with and without the optional engines, on Python 3.9 and 3.13, and a nightly job that fuzzes 20,000 malformed inputs. The published test count is not current: the README’s status section still reads “Tested with 208 unit tests” at v0.9.0, while pyproject.toml and the latest release are 0.11.0; a pull request opened on 2026-09-11 reports “377 tests pass locally”, with 62 optional-engine skips.

5. 05

   The other half: state that survives a reset

   The second job is keeping an agent’s context honest, and it has the more unusual design. v0.8.0 began writing the loop’s state to disk as it happens: .reverify/ledger/<sha256>.json, one ledger per binary, content-keyed so a renamed copy shares its ledger, checkpointed after every round, with refutations kept as KNOWN FALSE so a fresh context does not re-propose the same wrong prior — and only what a tool verified, observed, proved or refuted is written, with the model’s own notes excluded on purpose. reverify rollover applies the same rule to an interactive session in Claude Code, Codex, Gemini CLI or OpenCode: built-in compaction is turned off, the model writes a hand-off file with fixed sections, a guard at the harness’s stop hook blocks one stop and demands it, and a receipt is written only after the guard has checked that the hand-off was really rewritten and is well-formed — carrying the transcript’s SHA-256 and the user’s verbatim first and latest messages. install wires four harnesses, each with a backup and a matching uninstall; doctor reports receipts that no launcher consumed, which is the failure the documentation names: a session started outside the launcher “has no ceiling (one measured session reached 909k tokens before its owner noticed)”.

6. 06

   What the issue tracker did to the design

   Issue 14 is the tracker’s best round: an open-ended goal made the model drift off the structured kinds. On /usr/bin/ls, asked to “find the dynamic import list”, it produced 14 verified import_present claims; on /usr/bin/cat, asked for “the binary dynamically imports the close function from libc”, it produced no import claims at all and never finished, only raw byte reads. The cause was a RULES block in agent.py recommending only the raw kinds; the fix is one appended line, and the thread carries a before-and-after: 0 of 2 structured claims unpatched, 100% with the nudge. Pull request 11 shows the same standard from the maintainer’s side: he pushed the required changes onto a contributor’s branch rather than sending it back, one making native execution opt in. Against that, three reports about the verifier itself were unanswered at this record’s sampling: issue 22, where claims that assert nothing — an empty string, an all-wildcard pattern, zero bytes — come back VERIFIED and carry weight; pull request 21, the fix for it, open with only bot comments; and issue 23, where import_present silently degrades to a DLL-only check when the symbol field is misnamed and returns VERIFIED, reproduced the next day over MCP against notepad.exe. By the project’s own rule that is the most valuable report it can receive, and what its zero-false-accept number rests on.