What is the form of the program produced by this, is it native x86 or does K provide some sort of runtime/vm style elements? Does it fully encode all semantics

What is the form of the program produced by this, is it native x86 or does K provide some sort of runtime/vm style elements? Does it fully encode all semantics? Since typically formal verifications have issues with floating point stuff (hence why we STILL don't have complete formal models of C even in 2019). What is the performance like compared to traditional compilers? And to me the most important, what things can we suddenly do with K that we can't easily do with a combination of other tools, since it seems that it can do a lot more but this isn't really explained all that well to an outsider IMO.