Reverify turns binary claims into structured checks
Reverify accepts a claim such as a byte sequence at an offset, an imported function, or an expected register value, then asks a deterministic tool to judge it. The result is VERIFIED, REFUTED, or INCONCLUSIVE, accompanied by observed evidence. That is a better contract than asking a language model to sound certain about a PE, ELF, or Mach-O file. The model chooses what to investigate, while parsers and execution tools decide whether a specific statement survives.
The useful part is the boundary. Reverify does not promise that model prose becomes true. It defines structured claim kinds that software can check. Its ledger keeps verified, observed, proved, and refuted results across restarts, while leaving unverified notes labelled as such. Through MCP, an agent can call the same verifier without scraping terminal text. This is most convincing for reverse engineering, where an invented offset can send an analyst down the wrong branch for hours.
The zero-dependency core is smaller than the full analysis stack
The package metadata requires Python 3.8 or newer and declares 0 base dependencies. That core includes pure-Python readers and fallbacks. Higher-fidelity disassembly, emulation, parsing, and proofs come from optional Capstone, Unicorn, LIEF, and Z3 extras. Function boundaries, call graphs, cross-references, and reachability use angr through another extra that the project deliberately leaves out of full.
That separation makes a first trial cheap, but backend choice changes what a verdict means. Without the semantic engine, the README says the fallback can establish entry points and exports, while other semantic questions return INCONCLUSIVE. The CLI reports active backends, so save that output with any result you intend to share. A receipt tied to a lightweight fallback should not be presented as if angr recovered and checked a control-flow graph.
What happened when we ran it
Our sandbox installed commit f32ea84 in 23 seconds, adding 36 packages and consuming 37 MB on disk. The build succeeded in 1 second. Pip-audit reported 0 known vulnerabilities in the installed environment. Those are modest costs for trying the CLI or MCP server in a disposable workspace.
We did not run tests because the checkout exposed no test script or target. That is different from a failing suite: our harness had nothing it could invoke, so it produced no passing test count. The 1.5 MB checkout contained 109 files and about 17,503 lines of source, with 7 CI workflow files but no Dockerfile or tests directory. The repository may run checks through those workflows, but our result only proves that installation and build completed in the stated Debian container.
An open false VERIFIED report cuts into the central promise
Issue 23, opened September 23, reproduces a false VERIFIED outcome on PyPI version 0.10.0. An agent supplied symbol for an imported API name instead of Reverify's supported function field. Because the same claim also contained a recognized library field, the verifier silently reduced the request to a library-only check and returned success without judging the named symbol. The reporter reproduced the behavior through MCP as well as the CLI path.
This is not a complaint about fuzzy model interpretation. It sits on the exact boundary Reverify is meant to police: model-authored JSON entering a deterministic judge. Agents will misspell fields and choose plausible synonyms. Until unknown keys are rejected or clearly surfaced, callers should validate the claim schema, inspect the evidence, and confirm that the returned receipt mentions the fact they asked about. A green label alone is not enough.
Open-ended goals can stall before reaching the right claim kind
Issue 14 reports that one open-ended import question produced 0 import claims across 2 sessions. The model fell back to raw byte guesses, collected observations, and never completed the goal. Rephrasing the task around the structured import claim made the run converge in the reporter's example. An open pull request proposes a prompt change, but it was still unmerged when we checked.
This exposes a practical split between the verifier and the orchestrator. A well-formed claim can be checked deterministically, while the model still has to select the right claim kind. For important work, define the goal narrowly and watch the first round. If an import question produces offset guesses instead of import_present, stop and correct the task rather than paying for more unproductive turns.
Automatic rollover needs the launcher on Claude Code and Codex
Version 0.11.0 adds rollover support across 4 agent CLIs: Claude Code, Codex, Gemini CLI, and OpenCode. Reverify writes a fixed-shape hand-off file, records a receipt, and starts a fresh session where the host permits it. The design is sensible because verified ledger facts remain separate from the model's own notes.
The integration is not equal on every host. The README says plain Claude Code and Codex hooks can request and record a hand-off but cannot terminate their own session. Full replacement requires starting the CLI through reverify rollover, or configuring the documented successor route. Installation also edits each agent's configuration and disables native compaction, with backups. Run reverify rollover doctor after setup and after agent upgrades.
The project is active, young, and still alpha
GitHub listed 1,245 stars, 238 forks, and 8 combined issues and pull requests when fetched on September 27, 2026. The last code push was September 7, while issue discussion continued through September 24. The package metadata labels the project alpha, which fits the rapid release history and the unresolved verification defects better than the confident README headline does.
Packaging also trails the repository. GitHub marks v0.11.0 as the latest release, while PyPI currently reports 0.10.0. The release notes say the PyPI publish depends on enabling its trusted publisher. Reverify is worth trying because it makes an agent show its work in a form another tool can inspect. Keep the human in the loop until the verifier rejects malformed claims as firmly as it rejects wrong bytes.