TLA+ operates at a different level both conceptually and in the SDLC than programming languages like Dafny or Rust. TLA+ is a design language rather than an imp

TLA+ operates at a different level both conceptually and in the SDLC than programming languages like Dafny or Rust. TLA+ is a design language rather than an implementation language and this permeates a lot of its foundations. FWIW you can already use Dafny to write individual modules in real-world programs (it compiles to .NET and therefore interoperates with e.g. C#), although there are still some rough edges given the tiny size of its community, and the documentation for doing this is rather fragmentary. As for the difference between Dafny and Rust, Rust really has only one big unique trick up its sleeve which is its affine types. Otherwise its approach is entirely compatible with Dafny's (and indeed there are efforts to port over some the same ideas between Dafny to Rust, see e.g. https://alastairreid.github.io/rust-verification-tools/ https://alastairreid.github.io/rust-verification-tools/). Those will take a long time though to come to fruition because formal verification is still a hard problem.