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. Follow the instructions at: https://lean-lang.org/install/manual/ 1. Clone or download this repository git clone https://github.com/janmasrovira/mlda cd mlda Or download the zip file from: https://doi.org/10.5281/zenodo.18982928 2. Build and verify the proofs lake build The command above will: Automatically install the correct Lean version Download and build Mathlib4 (the standard mathematical library) 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 used in the formalisation but not in the paper are placed under the Lemmas namespace in each file. The generated documentation for this formalisation can be browsed locally or at janmasrovira.github.io/mlda. In the HTML documentation, theorem statements are presented without notation, which is 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