Right. But even the automatic translation/conversion from the "real" Python code (or whatever it is) to the toy model of that code would make TLA+ a lot more accessible and useful to millions of developers instead of the couple hundred at most (just a guess, maybe it's more?) that currently make serious use of it.

I understand that TLA+ is not really intended for that and it's currently used more for super important, mission critical applications like flight computer code, but I would love to see that level of care and attention brought to more typical software, which even in relatively "boring" applications can involve a lot of concurrency nowadays.

A toy model of existing Python code is... a type system, which Python has. TLA+ is appropriate for cases where you don't even have that.