Using State Charts as Models for Formal Verification

I've been looking at something called TLA plus, which is one of the more popular methods of formal verification. And so my heuristics are my assumptions of like how the app, uh, should look at any given state and, um, you know, all the actions I take. And based on that, I could automate the generation of integration tests where you're testing from starting the app to some end states. That sounds pretty awesome.