Comment by wucke13

For the seL4 proofs a subset of C was formalized, for example.

(Already mentioned) CakeML would be another example, together maybe with its Pancake sibling.

Also: WebAssembly!