Isn’t the Ada spec also not a formal spec?

The most popular language with a formal specification is Standard ML.

I guess this is terminology confusion on behalf of Surac, who probably just wants a specification that is independent of the rustc implementation.