2 papers
cs.SE2026
Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study
Jim Woodcock, Gabriel Leite, Augusto Sampaio +1
Large language models can propose proofs for interactive theorem provers, but a successful build does not show the surrounding verification task was preserved. We study this proble…
cs.SE2026
CAPRI: Contract-Aware Proof Repair for Isabelle
Jim Woodcock, Gabriel Leite, Augusto Sampaio +1
We address the use of large language models (LLMs) to help discover Isabelle proofs. An Isabelle build establishes that the submitted theory is accepted, but not that an LLM change…