Many languages can do that (Ada SPARK, Dafny, even Java with JML, and quite a few more), but there are really two languages here, the spec language and the program language. The spec language isn't executable, and the program language doesn't spec. What TLA+ does is offer a a single continuum, with a language that's much simpler than both Eiffel's spec language and its program language, and can describe anything at arbitrary precision. It can describe the QS algorithm in general, and it can describe the activations of the logic gates in the CPU as a specific QS runs on a specific machine, and it can take any description of QS, at any level, and show the abstraction/implementation between them. Again, this is all in a language that's much simpler than Python, and that allows reasoning directly in the language because it supports substitution and all the normal manipulation capabilities we expect from mathematical formulas.