> 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/outputs-and-the-coverage-ledger.md).

# Outputs and the coverage ledger

The five Devirt output formats (IDA database, annotated pseudocode, reverse engineering report, LLVM IR, structured JSON) and the coverage ledger's four outcomes: proven, runtime-dependent, unresolved

## Deliverables

| Output                     | Use it to                                                         |
| -------------------------- | ----------------------------------------------------------------- |
| IDA database               | Keep working in IDA, with functions already named and calls typed |
| Annotated pseudocode       | Read the recovered logic without opening a disassembler           |
| Reverse engineering report | Get the findings as written conclusions instead of code           |
| LLVM IR                    | Feed compilers and analysis pipelines                             |
| Structured JSON            | Drive automation and in-house tools                               |

The outputs that apply to a given file are named in its accepted offer.

## The coverage ledger

Each Devirt result carries a coverage ledger: an inventory of the code in scope in which every part receives exactly one of four outcomes.

![Devirt coverage ledger with the four outcomes: proven, runtime-dependent, unresolved and permanently bounded (illustrative example).](https://raw.githubusercontent.com/Devirt-re/.github/main/profile/devirt-ledger-light.svg)

| Outcome             | What it tells you                                             |
| ------------------- | ------------------------------------------------------------- |
| Proven              | It passed the comparison under the stated assumptions         |
| Runtime-dependent   | It needs a real input or environment before it can be settled |
| Unresolved          | The evidence available was not enough to decide it            |
| Permanently bounded | A stated limit rules out a stronger conclusion                |

Because the ledger names the exact build and its assumptions, a coverage percentage always comes with its limits attached.

## Read more

* [How to read a devirtualization coverage figure](https://devirt.re/research/devirtualization/coverage-is-a-contract)
* [Runtime-dependent, unresolved and bounded functions explained](https://devirt.re/research/devirtualization/runtime-dependent-functions)