Frama-C doesn't need to know anything about the target arch. It guarantees no undefined / implementation defined behavior on all architectures. You have to prov

Frama-C doesn't need to know anything about the target arch. It guarantees no undefined / implementation defined behavior on all architectures. You have to prove your code does not cause overflow/underflow (or accounts for it) if you add two integers or cast a uint32_t to an int32_t, etc. Very tedious, but it can and is being done. CompCert, the formally verified C compiler, is a separate thing from Frama-C, but currently supports x86, ARM, RISC-V, and PowerPC. (CompCert is actually mostly programmed in OCaml and the Coq/Gallina proof assistant.) CompCert guarantees that a correct ISO C program (no undefined or implementation defined behavior) is translated into an assembler program with the same semantics, i.e. an assembler program that computes the same results as the C source program. So CompCert for each supported architecture needs a formal semantics for any CPU instructions it generates. CompCert is an optimizing compiler and the optimizer accounts for the delay between when an instruction is issued and when the result is ready, accounts for pipelining and all that if that is what you are asking. But to write verified C programs you don't need to worry about instruction re-ordering happening lower down changing the meaning of your program and all that. That's a deeper layer of the onion, and, as Bjarne Stroustrup said, each time you peel a layer of the onion you cry more.