The code is already a formal spec.
Unless there are bugs in the language/compiler/interpreter, what the code is essentially formally well defined.
As programming languages get better at enabling programmers to communicate intention as opposed to being a way to generate computer instructions, there's really no need for a separate "spec". Any so called "spec" that is not a programming language is likely not "formal" in the sense that the behavior is unambiguously well defined.
Of course, you might be able to write the "spec" using a formal language that cannot be transformed into machine code, but assuming that the "spec" is actually well defined, then it's just that "compiling" the spec into machine code is too expensive in some way (eg. nobody has written a compiler, it's too computationally hard to deduce the actual intention even though it's well defined, etc.). But in essence it is still a "programming language", just one without a compiler/interpreter.
But right from the outset the approach is doomed to fail because its proponents write like they don't know what they are talking about and think they can write bug-free software.
It really should be "write software with a formal spec". Once people start talking about "proof" in practice it sounds dishonest. It isn't possible to prove software and the focus really needs to be on the spec.