Invariant to code translation, location in binary, and runtime

[KomaGR]

Investigate how to translate invariants to runnable code for checking conditions. How to implement the code and where to keep it in the final binary. When and how to perform the runtime checks based on the invariant specification.