Lean Binary Decision Diagrams
Eshel S. Yaron

Abstract:
We develop a formally verified Binary Decision Diagram library in, and for, the Lean 4 programming language and proof assistant.
Binary Decision Diagrams (BDDs) are a fundamental data structure for efficient representation and manipulation of Boolean functions. Popularized by Bryant in 1986, BDDs have been implemented and deployed in various applications of computer science and logic, including circuit design and verification, model checking, planning and constraint solving.
The significance of our contribution of a formally verified BDD library in Lean is threefold: first, spelling out subtle correctness proofs for key BDD algorithms in a fully formal setting elucidates the essential logical properties of the various interacting components in these algorithms. As Knuth (2009) remarks after describing his BDD reduction algorithm, “the intricate link manipulations of Algorithm R are easier to program than to explain.”
Additionally, the project has a practical benefit: a verified BDD implementation in Lean enables proof automation by leveraging Lean’s meta-programming facility. Namely, proofs of various statements about Boolean functions, such as satisfiability of a given propositional formula or semantic equivalence of two formulae, can be delegated to a verified, efficient, BDD-based decision procedure within Lean.
Lastly, a verified BDD library can be used as a component of verified BDD-based applications, such as verified model checkers whose correctness is formally proven in Lean. We implement and present a BDD-based SAT solver as an example application of our library.
We describe the library’s external API and its capabilities, explain the underlying implementation, discuss the design choices taken during formalization, and investigate implications of these choices. Finally we evaluate the performance of the presented implementation, compare it with other BDD implementations, and survey possibilities for further development.