> For the complete documentation index, see [llms.txt](https://devirt.gitbook.io/devirt/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://devirt.gitbook.io/devirt/how-devirt-works.md).

# How Devirt works

How Devirt recovers logic from VM-protected binaries: it traces the virtual machine, rebuilds its state and control flow, and checks every recovered function against the original.

A VM-based protector swaps a program's native instructions for bytecode that runs on the protector's own interpreter. Open that program in a disassembler or decompiler and the interpreter is what you see, not the logic. Doing the recovery by hand means rebuilding the dispatcher, identifying every handler and proving that each recovered function matches the original, all before the actual analysis can begin.

## From protected binary to checked functions

1. **Observe.** Devirt follows the protected program while it runs.
2. **Reconstruct.** It rebuilds the state and control flow of the virtual machine.
3. **Translate.** It turns that behavior into functions shaped like native code.
4. **Verify.** It compares each recovered function with the original program.
5. **Deliver.** The selected outputs arrive together with a coverage ledger.

## How recovered code is checked

| Check                 | Method                                                                                                                                          | Possible results                                                                                                                               |
| --------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------- |
| Solver check          | Searches a declared model for any input on which the recovered and original code disagree                                                       | UNSAT: no counterexample, which supports equivalence within the model. SAT: a disagreement was found. Timeout: the comparison stays unresolved |
| Differential check    | Lifts the recovered operations to LLVM IR, then compares them with recorded behavior of the original and with native execution on chosen inputs | A match on those inputs, or a documented difference                                                                                            |
| IDA persistence check | Saves the IDA database, reopens it and inspects it                                                                                              | Confirmation that function names and typed calls survive the round trip                                                                        |

Each check's outcome is written into the [coverage ledger](/devirt/outputs-and-the-coverage-ledger.md), function by function.

## The limits of a result

What you receive is inspectable logic; the original source code is never part of a delivery. A verified result holds for the declared scope and inputs, not for every behavior the program could show, and the ledger records the exact build and the assumptions behind it.

The full walkthrough is on [devirt.re/how-it-works](https://devirt.re/how-it-works).