Distributed Assertion Management Framework

The Distributed Assertion Management Framework (DAMF) is a proposed collection of formats and techniques to enable heterogeneous formal reasoning systems and users to communicate assertions in a decentralized, reliable, and egalitarian manner. An assertion is a unit of mathematical knowledge—think lemmas, theorems, corollaries, etc.—that is cryptographically signed by its originator.

The philosophy and beginnings of DAMF are explained in this technical report:

Farah Al Wardani, Kaustuv Chaudhuri, and Dale Miller (2023). Distributing and trusting proof checking: a preliminary report.

The technical construction of DAMF is explained in this paper:

Farah Al Wardani, Kaustuv Chaudhuri, and Dale Miller (2023). Formal Reasoning using Distributed Assertions (HAL). Appeared in the proceedings of the 14th International Symposium on Frontiers of Combining Systems (FroCoS), September 20–23, 2023.

DAMF is based on content-addressable storage using the InterPlanetary File System (IPFS) network, and uses the InterPlanetary Linked Data (IPLD) data model to represent assertions and all their components.

Explore the proposed DAMF Formats.

Read about Processes in DAMF.

Install Dispatch, an intermediary tool that helps in integrating systems.

Experiment with some edge systems. In particular:

• Abella DAMF, a version of Abella with DAMF support.
• λProlog integrated with DAMF.

Read an example walkthrough of using a heterogeneous combination of systems to prove an assertion.