Hmm, I wonder how well would formal verification work with LLMs. I'm not really a fan of vibe coding, but the little I know about formal verification, it could very well work as a way how to prove your vibe-coded slop isn't shit.

I've looked into formal verification once few years ago, but it's too much math and thinking for me to grasp. If I remember it right, I guess the problem would be that you'd (or, LLM would, in this case) have to correctly describe the code in the formal verification language, and it would have to match 1:1 with the code, which is a point of failure? So we'd be back to square one, but instead of having to verify every single line of code, you'd have to check the proof. But maybe I'm wrong.