Reference

What we do and do not claim

Every empirical statement on this site, paired with the overclaim it is routinely confused with. This page is the research package's own boundary table, rendered — not summarised.

A course built on twenty-one specimens and one 483-line program can say a lot of true things and almost no general ones. The distinction is not modesty, it is the subject: the two most instructive results here are a rewrite that looks correct and is not, and a lift that verifies and miscomputes. Both would have been reported as successes by anyone willing to describe their evidence loosely.

So the left column below is what the evidence supports. The middle column is the sentence people write instead — deliberately included, because recognising your own draft in it is the point. The right column is the evidence and the qualification.

Safe formulation	DO NOT SAY	Evidence / qualification
The 68 planned showcase matrix conditions linked as x64 PE and passed their canonical run checks.	All programs produced by these obfuscators are correct.	Matrix scope and commands. BinProtect and backend/MIR were not part of these 68 conditions.
Annotation-only SUB pilots for the tested OLLVM/Hikari compilers compiled without transforming the target; retained builds used global flags.	Hikari's retained matrix used validated function-local annotations.	Selective targeting result. Hikari flags: `-enable-subobf`, `-enable-bcfobf`, `-enable-cffobf`, `-enable-splitobf`, each via `-mllvm`. This does not prove annotation support is impossible in every Hikari build.
All 24 intended OLLVM SUB O0 sites expanded in retained IR, but native XOR/SUB operations were already recognizable; higher optimization recovered all 24 intended native operations.	IR expansion guarantees difficult machine code, or msynth recovered operations already simplified before it ran.	Arithmetic study, optimization. Coverage, template diversity and persistence are separate.
The exact Polaris MBA O0 target grows from 115 to 678 native instructions.	Polaris is universally stronger than every other obfuscator.	Metric definitions. Named target and matched compiler baseline; not whole-PE size or a hardness proof.
The extended isolated-site synthesis probe accepted 10/12 recoveries after SMT checks; two were UNKNOWN.	Synthesis solved the corpus, or UNKNOWN means equivalent.	Synthesis expansion. Keep this separate from complete-function tests.
No complete recovery occurred among 20 extracted obfuscated complex-return expressions in the tested AST/SiMBA paths; useful partial reductions occurred.	Composed MBA is impossible to simplify.	Complex arithmetic, family results. Four Polaris MBA extractions hit a flag-AST guard; these are extraction limits, not failed SMT equivalence queries.
Hikari O0 BCF injected conditional gates were folded before native predicate analysis; the four surviving Jccs were genuine.	Triton removed Hikari's injected O0 gates.	Triton study. Source/IR provenance separates injected versus genuine conditions. Hikari's exact BCF IR text also has legacy mixed-pointer syntax; direct compilation worked, reparsing did not.
All 22 tested OLLVM O0 and 16 Polaris O0 injected gates were proved one-sided by the retained generic Triton workflow.	Triton can remove all opaque predicates.	Triton report, summary, one frozen proof. Bounded exploration, supported memory semantics and recorded prefix coverage matter.
Under path prefix P, UNSAT for P ∧ not-C rules out that branch direction for states covered by P and the model.	One path-local UNSAT result establishes a global invariant for every program execution.	Proof methodology. Require feasible/reachable context and coverage of relevant prefixes. SAT gives a model; TIMEOUT/UNKNOWN is not proof.
Tigress O0's three injected gates became provable after importing one captured initialized state while x/y remained symbolic.	Tigress predicates are universally opaque for arbitrary global state.	Generic result, initialized result, state. Generic yield 0/3; initialized 3/3. Allocation, entropy, heap layout and subsequent mutations are not universally quantified by this model.
A separate proof consumer rewrote the 22/16 gates as JMP plus padding; all retained canonical and 9,189 native differential triples matched.	Triton's proof automatically produces a fully deobfuscated PE, or tests prove all inputs.	OLLVM validation, Polaris validation, rewrite report. Analysis and rewriting are distinct steps.
Audited entry-reachable BCF blocks fall 70→37 for OLLVM and 54→30 for Polaris; physical bytes and predicate arithmetic remain.	All dead code was deleted, or an unchanged file size means no deobfuscation happened.	OLLVM projection notes, Polaris notes. These CFGs do not split calls; Miasm's FLA counts do.
Stock ollvm-unflattener produced working canonical rewritten PEs for the selected OLLVM-16 O0 and Hikari O0 specimens.	Stock ollvm-unflattener generically supports all OLLVM-family flattening.	OLLVM result, Hikari result. 25/25 and 28/28 successor pairs; graph-pair scores do not prove branch polarity or every runtime behavior. O2 results differ.
Polaris's stock O0 FLA rewrite is WRONG despite a smaller 10-block graph.	Polaris FLA was successfully deobfuscated.	Stock result, wrong output: F9CD8332 instead of DBEFFCE7; exit 1. Legitimate switch alternatives become sequential operations. Static negative example only.
Stock Tigress Flatten discovery saw 6 blocks where the jump-table-aware reference has 38; no successful rewrite followed.	Tigress was reduced to six blocks, or the SMT solver failed to understand its semantics.	Discovery result, verified table. Failure occurred before useful symbolic successor recovery.
RPISEC's SSA def/use approach was inspected as an alternative methodology.	RPISEC was executed successfully on this corpus, or would fix Polaris automatically.	Methodology section. No Binary Ninja plugin run is claimed.
Mergen emitted verifier-valid, recompilable LLVM IR for all 17 selected cases at four retained stages (68 modules).	Verifier-valid lifted IR is semantically correct.	Mergen study, totals. Thirteen cases had passing runtime outcomes under their contracts; two BCF lifts were not run and BinProtect stayed static-only.
Mergen's lift of the valid native OLLVM SUB specimen is SEMANTIC FAILURE in all four stages.	OLLVM SUB's original executable is wrong, or ordinary LLVM O2 introduced the lifting bug.	Mismatch record: 3,917/4,118 mismatches per stage; raw lift already wrong; x=0 expects 0x08083808 but gives 0.
The retained Polaris MBA lift passes 4,118 vectors per stage yet retains substantial MBA (359 M2 IR instructions).	Mergen recovered clean source or rewrote the original PE.	Semantic result, IR metrics. R→R2 and R→M→M2 are alternative paths, not one four-stage chain.
All eight tested BinProtect protected outputs failed runtime validation by crash or hang.	BinProtect provides a working runnable course lane, or its static expansion proves superior protection.	BinProtect report. No protected BinProtect PE included. Virtualization was intentionally not tested.
Original PDB identifiers can survive rewriting while instruction mappings become stale.	Matching RSDS GUID/age proves original PDB mappings remain correct inside rewritten functions.	Rewrite metadata audit, unflattening report. No PDBs are included; use exports/RVAs and distinguish ordinary execution from unwind guarantees.
Optimization level changes both treatment survival and recovery-tool behavior.	Every O0 result transfers to O2, or cross-compiler counts form a fair leaderboard.	Optimization, boundary correction. Historical next-export measurements can overrun target boundaries; Tigress /Ox clean is 106 instructions, not the older O2 overcount.
Some retained seeded probes repeated identically; Polaris MBA/MIR and whole Tigress generated files did not reliably reconstruct from seed alone.	A seed is a complete reconstruction key for all passes.	Polaris validation, Tigress validation. Preserve exact artifacts and hashes.
Screenshots illustrate the graph/instruction views actually visible, with two explicitly held identity mismatches.	Filename, diff colour or visual similarity proves binary identity or semantic equivalence.	Visual index. Exact screenshot capture tool version/database hashes were not supplied.

The scope checklist

The same document ends with the checklist every page here was written against, and the one A1, A2 and the capstone are marked against:

name the specimen and the optimisation level;
identify the representation and the metric convention;
link the retained evidence;
state the relevant input and state assumptions;
distinguish SAT, UNSAT and UNKNOWN;
say whether an executable was actually produced, and whether it was validated.

Four things this site will never say

That the Polaris flattening rewrite worked. It produces a smaller graph and the wrong answer, and it is on this site as a failure.
That a smaller control-flow graph is evidence of correct deobfuscation.
That verifier-valid LLVM IR is evidence of a faithful lift. One retained lift is verifier-clean and wrong on 3,917 of 4,118 inputs.
That a BinProtect protected output is a working sample. All eight tested outputs crashed or hung.