I love the concept of formal verification, but translating my algorithms into yet another DSL and hoping I get that right seems like a waste of time. I'd rather simulate the algorithm with my brain.
Good luck with this. I heard about practical TLA usage. There was hang up in python asyncio library related to concurrency and it required 24 steps to reproduce. It was found and fixed with TLA help.
