[weitendorf]

Nothing stops you from writing a formal spec for an implementation or the technical parts of a problem that the product / upstream requirements don't explicitly demand. In fact I would say this is a large part of what software engineering fundamentally is; the reason specs are written in a certain way is because they model a problem domain and encode fundamental (or incidental, which could still be very well-reasoned, eg due to backwards compatibility, limitations of dependencies, or practical constraints) properties that are unlikely to change. Once you've actually written software that other systems/components are depending on, you've in practice created a spec. And it's a false dichotomy to think that just because there is no formalized spec for something before it's implemented at all, that this means that once the domain is better understood or stabilizied, you cannot use formal verification on the de-facto spec that has been arrived at/de-jure rules and structure that are prescribed but not yet formalized.

Even when you are writing something for the first time, like a parser for a certain kind of data format, you often can greatly accelerate your production-safety/security maturity by formalizing your spec enough to be fuzzed and to use existing parsing tooling that avoids the footguns most developers will introduce writing their own parsers from scratch. This is IMO the most common situation in which formal verification becomes very useful; even if the data format is purely an implementaton detail, any time parsing untrusted/user-provided input is involved, it would be much more foolish to try to just throw together some random string processing functions than to use something like flex/bison, an existing serialization format/protocol, or a metaparser (which may themselves be formally verified).