Will the TLA+ spec Claude spits out do what the users actually desire? Will there be human oversight of the spec? If not, I don't see how it really helps if the future human machine interface is supposed to be loosey goosey natural language. The best thing I can conceive is some human observers of the system saying "Claude, the behavior as it stands now is perfect! Set it in stone with TLA+." But this whimsical idea has many problems.