SW_GruVe - A Verified Proof Checker for Isabelle

Chair for Logic and Verification

Overview

In addition to following the LCF principle, the generic proof assistant Isabelle can already emit proof terms. This project aims to develop a formally verified proof checker for these terms, in order to further increase trust in the system.

For this, we aim to develop a formalization of Isabelle’s metalogic, define an (efficient) proof checker and verify the checker with respect to the metalogic. Using the resulting tool, we plan to check existing proofs, for example from the Isabelle distribution or the Archive of Formal Proofs. Further goals include the handling of compressed proof terms and ensuring absence of circular dependencies in user definitions.

This project is part of SW_GruVe (Erweiterung der Grundlagen für formale Verifikation von Software und deren Anwendung), a joint project with Hensoldt Cyber and UniBW. SW_Gruve aims to improve tools for formal verification and use them exemplary for verifying safety critical components of operating systems.

Funding: Wirtschaftsministerium Bayern under DIK-2002-0027//DIK0185/03

Bibliography

  1. Tobias Nipkow and Simon Roßkopf. Isabelle’s Metalogic: Formalization and Proof Checker. In: Automated Deduction – CADE 28. CADE 2021, LNCS