The behavior of the generated binary can be verified against the requirements. Yeah, the most common way to do this is to verify certain properties at the source code level, and then rely on various ways to show equivalence between the source code and the generated assembly, the generated assembly and the generated binary, and the formal semantics of the generated binary and the as-executed semantics on the chosen hardware; but it's perfectly reasonable, and not even particularly unusual, to skip the first equivalence and verify the assembly against the requirements directly.
The behavior of the generated binary can be verified against the requirements. Yeah, the most common way to do this is to verify certain properties at the source code level, and then rely on various ways to show equivalence between the source code and the generated assembly, the generated assembly and the generated binary, and the formal semantics of the generated binary and the as-executed semantics on the chosen hardware; but it's perfectly reasonable, and not even particularly unusual, to skip the first equivalence and verify the assembly against the requirements directly.