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?
They're probably referring to tech like reasoning models, or agent harnesses for example, which are arguably slowly moving things towards the symbolic end of the spectrum.
LLMs using REPL are one instance of symbols to "bounce" their prediction against domain constraints for verification. Also shout out to Gary Marcus who was right after all (and LLM companies wasting 100s of billions of dollars for years in-between on pure scaling).
I had tried to get long term memory out of Claude by indexing my notes with keywords and putting that in a sqllite database and Claude queries using full text search. Don't know how good it is, it seems to find things alright. My goal was to keep context small and only get Claude to ask for what it needs. Datalog seems like a great idea, will definitely try it out
The rewrite was a lot faster. Actually shaking out the bugs from the rewrite (or just getting enough confidence in the new version from use by early adopters) is probably not going to be drastically faster.
reply