Strangely enough, TLA+ and other formal proofs work very well for driving Ralph.

I would consider that expected but not strange. The thing blocking adoption is that most devs/people find those formal languages difficult or boring. That's even true of things like Cucumber - it's boring and most organizations care little for robust QA.