riscv-coq VS rtasm

>it allows to formally verify the correctness of a particular ISA

That must be hypothetical. Functionalness of the language doesn't make anything that is written in it automatically subject to formal verification. (mechanized or pen and paper). What kind of correctness properties does it actually allow to formally verify? I understand if it was the F* language, which is a full blown dependently typed proof checker, but with F#, which is defined by the implementation and 300 page English spec, I don't think you can verify anything interesting. As far as I know F# itself doesn't have mechanized formal semantics and its type system could be unsound.

https://github.com/mit-plv/riscv-coq and https://github.com/riscv/sail-riscv (don't know how complete they are) approaches actually allow to formally (mechanically) verify riscv properties.

I created this for x86 many years ago: https://github.com/kristiandupont/rtasm

It's not an emulator, it allows you to assemble code in C++ at runtime. It breaks down the architecture (as it looked at the time) quite detailed, if you are interested :-)

I experimented with this for native x86 many years ago (https://github.com/kristiandupont/rtasm). I used it to generate BitBlt functions with no conditionals in the hot paths, which created noticeable performance improvements with no compromise in flexibility. Debugging code like that is painful though!