Has anyone tried formal verification with AI generated code? I can't convince my company to use it but I realise it's very easy to ask Claude to add a verification step locally on my own PRs
At one point I was using TLA+ but it just made the problem "is the spec right?" or "does the code match the spec?". I could ensure that the properties defined in the spec were valid, but that didn't seem to translate into confidence that my code was correct. Maybe I was holding it wrong, it was just an experiment in an area I'm unfamiliar with.
Ultimately I have stuck to the informal verification of defining my expectations and ensuring that tests cover them.
I don't know TLA+ but indeed that seemed to be the limitation when I read about it too. What about languages like Dafny, that allow you to "prove" your programs?
Comments
Has anyone tried formal verification with AI generated code? I can't convince my company to use it but I realise it's very easy to ask Claude to add a verification step locally on my own PRs
At one point I was using TLA+ but it just made the problem "is the spec right?" or "does the code match the spec?". I could ensure that the properties defined in the spec were valid, but that didn't seem to translate into confidence that my code was correct. Maybe I was holding it wrong, it was just an experiment in an area I'm unfamiliar with.
Ultimately I have stuck to the informal verification of defining my expectations and ensuring that tests cover them.
I don't know TLA+ but indeed that seemed to be the limitation when I read about it too. What about languages like Dafny, that allow you to "prove" your programs?