Just because there isn't a formal spec, doesn't mean that the underlying systems aren't built with some rules, grounded in computer science and math. We believe that the systems we've set up do guarantee those properties, even if they haven't yet been formally verified. And a subset of them have been formally verified, which also increases confidence.
Adding to that confidence level is empirical results: while people have found implementation bugs, which will always exist in any implementation, nobody has managed to demonstrate that the model is fundamentally broken. That it's been years, and many people have tried, also leads us to suspect that our conclusions are correct here.
Put another way: not all specs are equal. Some are formal, some are informal. Just having a spec doesn't actually guarantee anything either. Most languages don't have a specification at all.