Ben Lorica asked what a buyer should ask to make sure a vendor isn't overselling "formally verified" AI-generated code. De Moura's answer: a proof is only as meaningful as the specification it proves, and a trivial spec proves nothing.
Yes.
So, what are some of the key questions you need to ask me in order to make sure that I'm not BSing you?
Show me the specification. Show me your specifications, the properties, what you have verified, right? Someone can formally verify my property is just true. It's basically saying there's no property. You are not making any claim. I think you're absolutely right that we should be aware of claims like my code is formally verified without explaining exactly which properties have been verified. What's the specification you verified against?
What proof checker kernel did you use?
Exactly. It's also important, right? Each tool. Another one that should be important, the trusted code base. There are tools that have a large trusted code base in Ling and other proof assistants like Rock, Isabel. This just focus on the trusted code base should be really small, right?
Yeah, yeah, yeah. And obviously, to the extent that you can convince me that your software has run in a similar setting, in other words, a realistic setting, maybe that adds to the meat behind the verification claim, right? So, what about, you know, we talk about software as if, you know, they're…