Metadata-Version: 2.4
Name: reverify
Version: 0.9.0
Summary: Anti-hallucination for AI agents that read binaries: the model proposes, deterministic tools decide. Claims verified or refuted against the real bytes, with evidence; grounded facts survive context resets. MCP server + CLI.
Author: 2akouwu
License: MIT
Project-URL: Homepage, https://github.com/2akouwu/reverify
Project-URL: Repository, https://github.com/2akouwu/reverify
Project-URL: Issues, https://github.com/2akouwu/reverify/issues
Keywords: anti-hallucination,hallucination,grounding,verification,llm,ai-agents,context-engineering,mcp,reverse-engineering,binary-analysis,disassembler,frida,protobuf,malware-analysis,ctf
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Topic :: Security
Classifier: Topic :: Software Development :: Disassemblers
Requires-Python: >=3.8
Description-Content-Type: text/markdown
License-File: LICENSE
Provides-Extra: capstone
Requires-Dist: capstone>=5.0; extra == "capstone"
Provides-Extra: unicorn
Requires-Dist: unicorn>=2.0; extra == "unicorn"
Provides-Extra: lief
Requires-Dist: lief>=0.14; extra == "lief"
Provides-Extra: z3
Requires-Dist: z3-solver>=4.12; extra == "z3"
Provides-Extra: angr
Requires-Dist: angr>=9.2; extra == "angr"
Provides-Extra: full
Requires-Dist: capstone>=5.0; extra == "full"
Requires-Dist: unicorn>=2.0; extra == "full"
Requires-Dist: lief>=0.14; extra == "full"
Requires-Dist: z3-solver>=4.12; extra == "full"
Provides-Extra: dev
Requires-Dist: pytest>=7.0; extra == "dev"
Dynamic: license-file

<h1 align="center">Reverify</h1>

<p align="center">
  <strong>The AI proposes. The bytes decide.</strong><br>
  Anti-hallucination for AI agents that read binaries: every claim is checked against the real bytes.
</p>

<p align="center">
  <a href="https://pypi.org/project/reverify/"><img src="https://img.shields.io/pypi/v/reverify?color=3fb950" alt="PyPI"></a>
  <img src="https://img.shields.io/pypi/pyversions/reverify" alt="Python">
  <img src="https://img.shields.io/badge/tests-196%20passing-3fb950" alt="Tests">
  <a href="LICENSE"><img src="https://img.shields.io/github/license/2akouwu/reverify" alt="MIT"></a>
  <img src="https://img.shields.io/github/stars/2akouwu/reverify?style=social" alt="Stars">
</p>

<p align="center">
  <a href="https://app.ona.com/#https://github.com/2akouwu/reverify">
    <img src="https://ona.com/build-with-ona.svg" alt="Build with Ona" />
  </a>
</p>

Ask an AI to reverse-engineer a file and it will make things up — offsets, structs, what the
code does — and say it like it's fact. Reverify checks it against the one thing that can't lie,
**the bytes**. Every claim is tested against the real binary; only what's true survives.

On 19 real Windows system files, the AI's textbook answer was wrong **100% of the time** —
reverify caught every one, with **zero false alarms**
([EXAMPLE.md](EXAMPLE.md), [BENCHMARK.md](BENCHMARK.md); `python benchmarks/prologue_prior.py`).

<p align="center">
  <img src="docs/demo.svg" alt="Reverify catches the model's hallucinated prologue on kernel32.dll, then verifies the corrected claim" width="760">
</p>

## 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.
- **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](SECURITY.md).

## Quick start

```bash
# 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:

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

```bash
# 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](#the-semantic-layer-functions-calls-and-cross-references)). 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.

### Grounded means *informative*, not just "nothing refuted"

"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](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](BENCHMARK.md) is the reproducible measurement behind the numbers above.

## 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.

```bash
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 semantic layer: functions, calls and cross-references

Bytes, instructions, imports and emulation are what the deterministic core can judge on
its own. The claims analysts actually make — *function X calls Y*, *this string is
referenced from that routine*, *this code is reachable from the entry point* — need
function boundaries and cross-references, which means a real program-analysis engine.
Reverify does not build one. It stands on **angr** (`pip install "reverify[angr]"`) and
keeps its own part thin: an engine-neutral view of functions, call edges, data references
and reachability, and four claim kinds checked against it.

```bash
reverify functions msimg32.dll                                 # what the engine recovered
reverify verify msimg32.dll \
  --claim '{"kind": "calls", "params": {"from": "AlphaBlend", "to": "SetLastError"}}' \
  --claim '{"kind": "references", "params": {"to": 12632, "space": "rva", "from": "AlphaBlend"}}' \
  --claim '{"kind": "function_at", "params": {"offset": 4112, "space": "rva"}}' \
  --claim '{"kind": "reachable_from_entry", "params": {"name": "DllInitialize"}}'
```

A refuted `calls` lists the function's real callees and a refuted `references` lists the
functions that do reference the address, so a model can fix the claim instead of guessing
again. `observe: true` reads instead of asserts (a function's size, blocks and callees; the
referencing functions of a string).

Honesty about strength: a recovered control-flow graph is *analysis-derived* — CFGFast is
heuristic and can miss or split functions — so semantic verdicts name the engine and are
recorded at a **`DERIVED`** tier below `VERIFIED`. Without an engine the pure fallback only
knows what is independently certain (the entry point and the exports are function starts)
and answers `INCONCLUSIVE` for everything else, never a guess. And the engine is checked the
way the readers are: the export table, parsed independently of angr, must agree with the
functions it recovers.

## The toolkit

| Command | What it does |
|---|---|
| `reconstruct` | **Closed loop: a model proposes claims, the tools verify, iterate until grounded** |
| `verify` | **Check a claim about the binary against the tools — VERIFIED / REFUTED / INCONCLUSIVE** |
| `verify` (behavior_equiv) | **Run the original function and a candidate over shared inputs; a mismatch returns a counterexample** |
| `auto` | Auto-triage: detect format, architecture, sections, top strings |
| `parse` | PE / ELF / Mach-O: arch, entry, sections, imports, exports (lief when installed) |
| `parse-pe` | PE32/PE32+ headers, imports, exports |
| `backends` | Show which engines are active (capstone / unicorn / lief) |
| `disasm` | x86/x64 disassembly of hex or a section |
| `pattern-scan` | AOB scan with `??` wildcards |
| `strings` | ASCII + UTF-16LE extraction with offsets |
| `emulate` | CPU register/stack micro-emulation |
| `decode-protobuf` / `decode-tlv` | schema-less wire-format dissection |
| `gen-hook` | Frida interceptor script generation |
| `hexdump` | aligned hex dump |
| `diff-patch` | binary diff / patch generation |
| `audit-boundary` | defensive filesystem/SSRF boundary audit |

## MCP server

Reverify exposes the toolkit to AI agents over the Model Context Protocol:

```bash
python reverify/mcp_server.py
```

Point Claude Code or Cursor at it and the agent can parse, disassemble, and scan binaries
directly — with the deterministic tools as ground truth. The `re_verify_claim` tool exposes
the verification loop, so an agent can have its own hypotheses judged against the bytes
before it reports them — and records every grounded result in the binary's ledger.
`re_ledger` restores that state after the host's own compaction or `/clear` (see
[The ledger](#the-ledger-state-that-survives-a-context-reset)); ledgers are also exposed as
`reverify://ledger/<sha>` resources.

## Status

**v0.9.0 — the semantic layer**, on [PyPI](https://pypi.org/project/reverify/)
(`pip install reverify`). The tool-grounded judge — a claim about the binary is checked
against the actual bytes and returned as `VERIFIED` / `REFUTED` / `INCONCLUSIVE` /
`OBSERVED` / `INVALIDATED` with evidence — ships as `reverify verify` and the
`re_verify_claim` MCP tool, and `reverify reconstruct` closes the loop. v0.3.0 brought the
mature engines (capstone, unicorn, lief); v0.4.x hardened the loop against gaming
(information-weighted scoring measured from the binary, address spaces, typed reads,
observe-then-assert, dependencies) and added a testbed that cross-checks the readers
themselves (pure parser vs lief on real binaries, disassembler/emulator vs capstone, Unicorn
and known-answer vectors, plus fuzzing). **v0.5.0** adds the strongest grounding — the
`behavior_equiv` claim runs the original function and a candidate reconstruction over shared
inputs and compares outputs, returning a concrete counterexample on a mismatch (the ExeBench /
LLM4Decompile re-executability methodology). **v0.6.0** makes the reconstruction loop two-stage
(observe, then hypothesize) with an established-facts ledger: only what the tools verified or
read is carried between rounds, so the model can't build on its own earlier guesses — the
defense against context hallucination. **v0.7.0** adds a proof tier: the `prove_equiv` claim uses
Z3 to prove two expressions equal for *all* inputs (verifying MBA deobfuscation), giving an honest
strength ladder — proven > tested > observed. **v0.8.0** makes the loop's state durable: a
per-binary ledger of what the tools verified, observed, proved and refuted, checkpointed every
round and restored after `/clear`, compaction or a restart — lossless by construction, because
nothing the model said on its own was ever kept. **v0.9.0** adds the semantic layer on angr:
function boundaries, the call graph and cross-references as `function_at` / `calls` /
`references` / `reachable_from_entry` claims, recorded at an honest `DERIVED` tier, with the
export table as an independent oracle for the engine. Tested with 208 unit tests, so the
verifier is not just trusted, it is checked.

## License

MIT — see [LICENSE](LICENSE).
