Modal Logic for Declarative Distributed Algorithms in Lean 4

A full Lean 4 formalisation of the paper “Declarative distributed algorithms as axiomatic theories in three-valued modal logic over semitopologies” by Murdoch J. Gabbay.

Overview

This formalisation includes:

• Section 2:
  • Three-valued logic: A three-valued logic with logical connectives and predicates
  • Semitopologies and modal operators: Finite semitopologies with modal operators □ (everywhere), ◇ (somewhere), ⊡ (quorum), ⟐ (contraquorum).
• Section 3: Logical expressions and models: Term and expression syntax, semantic models, and three-valued denotation
• Section 4: Broadcast algorithm: Bracha Broadcast specification and correctness proofs
• Section 5: Consensus algorithm: Crusader Agreement specification and correctness proofs

Repository structure

mlda/
├── Base.lean          # (Utility) Foundation
├── Base/
│   └── FinEnum.lean   # (Utility) FinEnum derivation macro
├── Section2.lean      # Three-valued logic: 𝟯 type, connectives, fold operations
                       # Finite semitopologies, modal operators, quorum properties
├── Section3.lean      # Term/expression syntax, models, denotation semantics
├── Section4.lean      # Broadcast algorithm specification and proofs
└── Section5.lean      # Consensus agreement specification and proofs

In the paper, Section 1 serves as an introduction, so it is not included in the Lean formalisation.

Verifying the proofs on your computer

First, you need to install Lean. You should follow the instructions at https://lean-lang.org/install/manual/

1. Clone this repository

git clone https://github.com/janmasrovira/mlda
cd mlda

2. Build and verify the proofs

lake build

The command above will:

1. Automatically install the correct Lean version
2. Download and build Mathlib4 (the standard mathematical library)
3. Build and verify all formalised proofs

Note that when compiling for the first time, the whole process can take up to 30 minutes

If the build completes without errors, all proofs are mechanically verified correct.

To confirm that it completed correctly, check that the last lines of output of the lake build command match the following:

ℹ [730/735] Replayed mlda.Section2
info: mlda/Section2.lean:17:0: Checking definitions and proofs in Section 2...
ℹ [731/735] Replayed mlda.Section3
info: mlda/Section3.lean:16:0: Checking definitions and proofs in Section 3...
ℹ [732/735] Built mlda.Section4
info: mlda/Section4.lean:16:0: Checking definitions and proofs in Section 4...
ℹ [733/735] Built mlda.Section5
info: mlda/Section5.lean:17:0: Checking definitions and proofs in Section 5...
Build completed successfully (735 jobs).

How to explore the formalisation

The structure of this repository mirrors the paper. Each section corresponds to a SectionN.lean file containing the relevant definitions and theorems. Every lemma, theorem, and corollary has its own namespace - for example, Theorem 2.4.5 is formalised in mlda/Section2.lean under the namespace Theorem_2_4_5.

Generic auxiliary lemmas that are used in the formalisation but do not appear in the paper are placed under the Lemmas namespace within each file.

The generated documentation for this formalization can be browsed at janmasrovira.github.io/mlda. In the HTML documentation, theorem statements are presented without notation (a limitation of the existing tooling). It is recommended to follow the Source link to see them presented with proper notation.

Building the documentation locally

To build the documentation run:

lake -d docbuild build mlda:docs

When the above command finishes, the documentation will be available at docbuild/.lake/build/doc/mlda.html.

License

This work is licensed under CC-BY 4.0.