v0.8.0 — lossless context rollover

Lossless context rollover

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. Reverify's loop can avoid that loss, because it already knows which part of the transcript is state — what the tools verified, observed, proved, and refuted. v0.8.0 writes exactly that to disk as it happens.

• Durable per-binary ledger (.reverify/ledger/<sha256>.json, REVERIFY_LEDGER_DIR): grounded results only, plus refutations as known false. Checkpointed after every round; content-keyed; atomic writes; corrupt files quarantined; unverified claim notes never stored.
• Resume anywhere: reverify reconstruct picks up from the ledger; a fresh context sees ESTABLISHED and KNOWN FALSE, so it neither re-derives facts nor re-proposes the same wrong prior. A claim already in the ledger scores zero (known).
• Bounded in context, unbounded on disk: --max-facts with proof-grade facts pinned; --prompt-budget trims the shown fact sheet deterministically (kernel32.dll: 43k chars fit a 20k budget). Scoring uses the full sheet.
• MCP: re_verify_claim records automatically; new re_ledger tool restores state after the host's /clear or compaction; server instructions; reverify://ledger/<sha> resources; protocol fixes (notifications, ping, real version).
• Claude Code hook: reverify ledger --hook prints a SessionStart (compact|clear|resume) hook that injects one index line per binary — the hand-off costs a few dozen tokens; facts are pulled on demand.
• 20 new tests, 196 total.

pip install -U reverify

v0.7.1 — bounded reconstruction ledger

The established-facts ledger is now capped (max_facts, default 40) so a long reconstruction run doesn't turn its own accumulated context into a fresh source of drift — long-session hygiene for the loop. Dropped facts were verified true and can be re-observed. 177 tests. pip install -U reverify

v0.7.0 — a proof tier (Z3)

Sampling says "no counterexample found over N inputs"; a solver says "no counterexample exists". This adds the second.

Added

• prove_equiv claim (Z3): proves two integer expressions equal for all inputs over bit-vector logic, or refutes with a distinguishing input — verifying MBA deobfuscation. (x^y)+2*(x&y) is proven equal to x+y for every 64-bit input; x^y==x+y is refuted with a counterexample.
• Z3 as an optional backend: pip install "reverify[z3]" (or [full]); INCONCLUSIVE without it.

Honest strength ladder: proven > tested > observed. 176 tests. pip install -U reverify

v0.6.0 — against context hallucination

Fights the model building on its own earlier guesses, and misremembering values from long context.

Added

• Established-facts ledger: only results the tools grounded (VERIFIED with weight, or OBSERVED) are carried between rounds. The model's own unverified claims are never carried forward; it's told to build only on BINARY FACTS + ESTABLISHED.
• Two-stage loop: each round the model first OBSERVEs what it needs but doesn't know (the tools read it), then HYPOTHESIZEs new checkable claims — separating what to investigate from what is true.

168 tests, including that a refuted hallucination and its note never reach the next round. pip install -U reverify

v0.5.0 — execution as judge

The strongest grounding: verify a function reconstruction by running it, not reading it (the ExeBench / LLM4Decompile re-executability methodology).

Added

• behavior_equiv claim: the original function (offset into the binary, or inline code) and a candidate (expr over x0,x1,... or candidate_code hex) are run over shared inputs and their outputs compared. A mismatch returns a concrete counterexample input; agreement is reported honestly as "equivalent over N inputs (tested, not proven)".
• Runs on Unicorn (x86-64 SysV convention by default), no compiler or model needed to verify. Behavioral equivalence is the highest-weighted claim; inline originals are self-referential (weight 0).
• Safe expression evaluator; CLI prints the counterexample.

163 tests. pip install -U reverify

v0.4.2 — who verifies the verifier

Cross-checks the readers the way mature tools do (Csmith, RISU, NIST vectors), and ships the bugs that found.

Added

• Differential + fuzz testbed: pure parser vs lief over real x64/x86 binaries; round-trips; malformed input never crashes/warns/false-verifies; soundness.
• Cross-engine oracle + KAT: hand-verified instruction vectors, pure decoder vs capstone, pure emulator vs Unicorn, engine fuzz. 151 tests.

Fixed (both found by the testbed)

• MicroEmulator raised on a wild esp+push from hostile code instead of faulting; now halts like Unicorn.
• Pure disassembler dropped bytes (uncounted REX prefix, truncated mov); now accounts for every byte.
• lief warning leak on malformed input suppressed.

pip install -U reverify

v0.4.1 — measured weights

Weights are measured from the binary, not tabled by claim kind: how often the expected content occurs in this file and its entropy. Zero padding, a ubiquitous prologue, or a pattern that matches everywhere now weigh ~0 even though they verify; emulation must execute non-degenerate code. Closes the padding exploit a fixed table allowed. evidence.weight_basis shows the numbers. 133 tests. pip install -U reverify

v0.4.0 — a loop that is hard to game

Scores what the verified set actually says, and closes the channels a model uses to look grounded without being informative.

Added

• Information-weighted scoring: weight 0 for claims restating the fact sheet, duplicates, self-referential inline code, and echoes of previous tool output. grounded = nothing refuted and verified weight ≥ --min-information. (CORE-style)
• Address spaces file|rva|va with translation + nearest_offset_of_expected; typed reads u16/u32/u64_at; OBSERVED verdict; id/depends_on → INVALIDATED; operands on instructions.
• Agent: addressed fact sheet with shift signals, echo/attrition detection, --samples with the verifier as selector.

Fixed

• Pure PE parser: PE32+ ImageBase misread (BaseOfCode width) and PE32 crash on every 32-bit binary. Pinned on both backends.

128 tests. pip install -U reverify

v0.3.0 — mature engines

v0.3.0 swaps the hand-rolled internals for battle-tested engines when installed, keeping the pure-Python core as fallback.

Added

• Optional backends: capstone (disasm), unicorn (real CPU emulation), lief (PE/ELF/Mach-O). pip install "reverify[full]"; reverify backends shows what's active.
• Unified reverify parse for PE / ELF / Mach-O (arch, entry, sections, imports, exports).
• Real x86/x64/ARM/ARM64 emulation via Unicorn; emulate --backend.
• New verifier claim kinds: import_present, export_present, section_present.

96 tests, gated to pass with or without the engines. pip install reverify

v0.2.0 — closed reconstruction loop

reverify reconstruct closes the loop: a language model proposes claims about a binary, the deterministic verifier judges each against the actual bytes, refutations are fed back, and it iterates until the reconstruction is grounded.

Added

• ReconstructionAgent (reverify/agent.py) and the reverify reconstruct --goal ... command (--mock offline demo, --rounds cap).
• Model injected as a propose callable; fully testable offline. openai_proposer() builds a live one from OPENAI_* env.

75 unit tests. pip install reverify