The most promising approach I've seen so far is... DST! First we simulate a system, we generate a bunch of timelines, then we see if those timelines are valid behaviors in the TLA+ design. I've heard of a few success stories and it's definitely cheaper than formal proof!
That’s just testing again. That’s not linking the code to the design.
DST feels to me like the way people treated memory access before Rust came around. Doing things properly was also seen as too costly then but now that it’s trendy everyone is fully behind lifetime tracking. Same here, formal proof is “too costly” but spray and pray approach like DST is somehow acceptable. Anyway, keeping with the Rust example I guess I just have to wait two decades and the next generation might finally see the light.
DST is the wrong solution to the actual problem. Its main advantage is that it doesn’t require that people used to design distributed system actually acquire new skill set and it doesn’t challenge the status quo too much (after all it’s pretty much just fuzzing on path you have chosen to make fuzzable).