Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study
CAPRI, a contract-aware proof-repair tool, is used to govern a reconstruction by combining Isabelle acceptance with an independent check of repository changes against machine-readable edit contracts, and the reconstruction discharged all ten scoped obligations within the original nine-theory structure.