Most companies now-a-days don't write spec up front. That's called Big Design up Front (BDUF) and it was seen in this industry that this was prone to failure which could cause the whole project to fail. That's because it's impossible to know everything up front and often during the project the requirements will change as the stakeholders learn of the consequences of their decisions.
In fact most companies don't do a "spec document" at all they design their system in small iterations called "sprints" typically 2-weeks and the "spec" is a ticket in a system like Jira (others are available). This process is part of Agile Project Management methods
> Everywhere I've worked where there were defined formulae (or formulae to be defined) this kind of thing was meticulously checked for correctness
There are some industries where they still do that kind of thing (BDUF) for example government work, defence, oil and gas. These are older industries that just haven't changed the way they approach projects. Amazon here is a bit a front runner when it comes to updating it's practices to be more leading edge so they likely adopted an Agile approach here learning about what was required as they go through the project.