Binary correctness
= Binary correctness
Conformance of compiled machine code to the behaviour of the code model used to justify it. <Binary correctness> can extend <formal verification> across the compilation step; the result applies to the particular compiled artifact and its assumptions.