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.
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
What even is the most complex programming language with a fully machine-checkable spec? Are there actually practically useful ones? I know of none.
One candidate is ATS [1].
Another, https://cakeml.org/
[1]: https://en.wikipedia.org/wiki/ATS_(programming_language)
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!
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.