[secos]

Talked with someone this morning who is using "formal methods" to validate their AI generated code.

They are using the same AI to generate the proofs.

[zby]

And how they are doing? I think this might be a solid research program - but that blog presented it as some kind of practical approach.

[janice1999]

That's why you should just subscribe to multiple LLM vendors. One model to write specs, one to write code against the specs and another to validate the code. Problem solved. (I have heard this proposed at work.)