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.

[–] rain_worl@lemmy.world 0 points 13 hours ago

you could make a program that verifies that the code matches the proof and that the proof is sound, but then you have to verify the program, and verify the verification, and verify your system of logic is consistent, which by gödel's incompleteness theorem is impossible(?)

[–] Barracuda@lemmy.zip 4 points 2 days ago

The LLM will just make up lies in the formal verification.