When using LLMs to modify formal proofs, you need independent verification beyond just checking if the code compiles—CAPRI shows that contract-based auditing can catch unauthorized changes that Isabelle alone would miss.
CAPRI is a system that uses LLMs to help repair broken Isabelle proofs while ensuring developers maintain control over what gets changed. It combines Isabelle's proof checker with an independent contract enforcer that tracks all changes, keeping an audit trail of prompts, proposals, and verdicts.