One 2026 preprint [L18], on a security proof developed by researchers working with AI agents and checked by the Lean proof assistant, reports: review of the definitions caught an AI-generated protocol that computed the key from both parties' strings combined, which neither party held on its own. Under the security definition alone, a protocol that always aborts would count as "secure"; the definition is paired with a bound on how often an honest run aborts. The protocol assumes an authenticated channel, as the paper states openly; a list of the axioms a proof uses would not show an assumption like that.
Before relying on "proved": read what was proved, and under which assumptions.
[L18] Ben-Shahar, Morag, Englund and Sulimany (2026), preprint.