Hi all,
I am trying to understand how proof assistants can be broken, in light of increasing use of AI agents. In particular, I am aware of ways in Lean where we can write (malicious) tactics that can be used to prove falsehood, that have no easy way to detect. In other words, this kind of vulnerabilities does not involve inserting axioms or in other similar ways, and genuinely makes the kernel to believe the existence of a proof of falsehood. This kind of problems can potentially detected by other mechanisms, but most likely not by ways built in the systems. In Lean, comparator provides an extra layer of guarantee, provided the fact that Lean’s tactic system allows various ways to prove falsehood, in case of not trusting the default lean kernel. To what I understand, this tool is a re-type-checker.
My question is: are you aware of any other this kind of vulnerabilities, in Rocq, Agda, Lean, Idris, or other proof assistants that you have experience with? I am trying to understand, whether any other proof assistants are exposed to this level of vulnerabilities, due to intentionally exposed API which bypasses the type-checker.
I intend to believe that Rocq is built with certain disciplines that prevent similar problems from occurring by constructions, but honestly, I do not write Rocq plugins or know much about Rocq’s internals. It would also be interesting, if you could share your opinions and stances about problems of such kind.
I am also sorry about cross posting, but without coq-club, I no longer know how to get enough number of people involved in a discussion.
Thanks,
Jason Hu