Formal Reasoning Using Distributed Assertions

When a proof system checks a formal proof, we can say that its kernel asserts that the formula is a theorem in a particular logic. We describe a general framework in which such assertions can be made globally available so that any other proof assistant willing to trust the assertion’s creator can use that assertion without rechecking any associated formal proof. This framework, called DAMF, 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. DAMF achieves a high level of distributivity using such off-the-shelf technologies as IPFS, IPLD, and public key cryptography. We illustrate the framework by describing an implemented tool for validating and publishing assertion objects and a modified version of the Abella theorem prover that can use and publish such assertions.