[wucke13]

Neither the Rust nor the Ada spec is formal, in the sense of consumable by a theorem prover. AFAIK for Ada Spark, there is of course assumptions on the language semantics built-in to Spark, but: these are nowhere coherently written down in a truly formal (as in machine-readable) spec.

[shakna]

There was also Larch/Ada [0], which was a formally proved subset of Ada, developed for NASA [1].

[0] https://apps.dtic.mil/sti/tr/pdf/ADA249418.pdf

[1] https://ntrs.nasa.gov/citations/19960000030

[Sharlin]

What even is the most complex programming language with a fully machine-checkable spec? Are there actually practically useful ones? I know of none.

[nine_k]

One candidate is ATS [1].

Another, https://cakeml.org/

[1]: https://en.wikipedia.org/wiki/ATS_(programming_language)

[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!

[gpm]

There's a formally verified C compiler, IIRC the frontend isn't, but if you define the language to the structs that are in the inputs to whatever is formally verified I guess whatever C like dialect of a language it implements must be.