[inigyou]

Great then let's prove that ASM is correct.

the reference C code is just as bad.

[pjmlp]

Which is actually possible, unfortunately the industry never cared that much about strong typed assembly.

See Verve OS from Microsoft Research, TAL and the origins of the Dafny language.

[inigyou]

It's smallish snippets that implement self-contained algorithms, which should make it well within reach of direct formal proof of correctness.