Tuesday 11 July 2023, 14:00, room 3U47: Formal Reasoning using Distributed Assertions, Farah Al Wardani (LIX, Inria).

When a proof system checks a formal proof, we can say that the kernel asserts that the formula is a theorem in a particular logic. We describe a general framework in which such assertions can be made global so that any other proof assistant willing to trust the creator of the assertion can use that assertion without rechecking any associated formal proof. This framework is heterogeneous and allows each participant to decide which tools and operators they are willing to trust in order to accept external assertions. This framework can also be integrated into existing proof systems by making minor changes to the input and output subsystems of the prover. It achieves a high level of distributivity using off-the-shelf technologies: IPFS, IPLD, and public key cryptography. We illustrate the framework by providing implementations of an intermediate tool for validating and publishing assertion objects and a modified version of the Abella theorem prover that can use and publish such assertions. More information can be found at the following website: https://distributed-assertions.github.io/