formal methods like TLA+/BPMN describe system behavior, while the specs document individual changes. these complement each other rather than competing from my point of view.

but yes, it would be great to able to have such kind of formal description. code is not standardized enough for that (by now)