zlacker

I haven't seen enough mention of using these tools to generate formal verification specs for their output, like TLA+. Of course, you're stuck with the same problem of having to verify the specs but you'll always be playing this game and it'd seem like this would be one of best, most reassuring ways to do so.

I'll have the look into this some more but I'm very curious about what the current state of the art is. I'm guessing it's not great because so few people do this in the first place -- because it's so tedious -- and there's probably not nearly enough training data for it to be practical to generate specs for a JavaScript GQL app or whatever these things are best at generating.