Formally verifying digital circuits with category theory in Lean

Circuits ❤️ Category theory

Digital circuits have a suprisingly beautiful model in category theory that are easy to understand but powerful enough to prove properties about real-world systems.

By modeling a circuit with category theory we get a strict guarantee that it is correct by construction by proving it adheres to the axioms of categories. Since a category is comprised of objects and morphisms between them, we can model a digital circuit with objects as numbers of wires and morphisms as circuits connecting them.

If you don’t know much about circuits or category theory that’s OK! We’ll go about building the circuit for an adder that adds binary numbers from first principles using circuitlib.

Categories of circuits

We’ll focus on combinational circuits which are simple because they don’t carry state, meaning that they can be denoted as ordinary functions. We can define a combinational circuit as a symmetric monoidal category with objects as numbers of wires and morphisms as functions between groupings of wires¹. By using four-value logic², short-circuits and disconnections in wires can also be modelled.

Specifically, to model real-world circuitry, they are Monotone functions.

Sequential circuits can be modeled as causal stream functions ¹, other complex real-world circuits are asynchronous and modeling them is an open area of research, if you figure it out please HMU!

Monoidal categories

First we’ll need to know a little bit about monoidal categories. These give us a clean way to compose circuits in parallel (by stacking them side-by-side with ⊗ operations) while guaranteeing that the wiring is well-formed.

≫ is category composition operator, which in this case is isomorphic to function composition. It wires the output of one circuit into the input of the next.

◁ and ▷ are the whiskering operators for monoidal categories. They let us “slide” a circuit past a parallel section without changing the overall behaviour.

α_ is the associator operator for monoidal categories. It lets us safely regroup three parallel bundles of wires, i.e. turning ((A ⊗ B) ⊗ C) into (A ⊗ (B ⊗ C)) (or the other way around), while keeping the actual signals and behaviour of the circuit completely unchanged.

We’ll use the two key laws from monoidal categories to help us verify we’re modeling valid circuits:

1. Pentagon law

   

   This law states that when you put three circuits in parallel, it doesn’t matter how you group them. In other words, the way you bundle parallel wires never affects the final result.

   ((A ⊗ B) ⊗ C) ⊗ D can be reassociated to A ⊗ (B ⊗ (C ⊗ D)) using only the associator α_.

   pentagon :
     ∀ W X Y Z : C,
     (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom =
     (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom
   

2. Triangle law

   

   This law tells us how the identity circuit (a bundle of wires that does nothing) interacts with parallel composition. It guarantees that adding an empty parallel section on one side and then cancelling it is a no-op.

   triangle : ∀ X Y : C, (α_ X (𝟙_ _) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y
   

Braided monoidal categories

Next we’ll take a look at braided monoidal categories. These give us the ability to safely cross wires in a circuit so that outputs reach the correct inputs.

The two important laws for braiding here are the hexagon laws. They ensure that crossing wires interacts properly with the associators (the regrouping of parallel wires) in a consistent way. In practice, this guarantees that wire crossings remain predictable no matter how you group parallel sections.

β_ is the notation for braiding which we use here to cross the inner wires in the circuit

1. Hexagon law

   

   hexagon_forward :
     ∀ X Y Z : C,
     (α_ X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
     ((braiding X Y).hom ▷ Z) ≫ (α_ Y X Z).hom ≫ (Y ◁ (braiding X Z).hom)
   

2. Hexagon inverse law

   

   hexagon_reverse :
     ∀ X Y Z : C,
     (α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
     (X ◁ (braiding Y Z).hom) ≫ (α_ X Z Y).inv ≫ ((braiding X Z).hom ▷ Y)
   

Symmetric monoidal categories

Finally, we’ll look at symmetric monoidal categories. These add one final crucial guarantee on top of braided monoidal categories: braiding is symmetric. In circuit terms, crossing two bundles of wires one way and then crossing them back the opposite way gets you exactly back to the original wiring.

1. Braiding symmetry law

   

   symmetry : ∀ X Y : C, (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
   

Circuits in lean

That’s enough hooplah about math stuff, let’s actually make something! Let’s write out some lean to prove things about the circuit of an adder that performs addition of binary numbers.

Let’s first understand how circuits can be used with the notation from category theory. First we’ll examine the primitive gates used to operate on four-value logic, often referred to as Belnap gates².

abbrev and : (ofNat 2 : C) ⟶ 1

abbrev or : (ofNat 2 : C) ⟶ 1

abbrev not : (ofNat 1 : C) ⟶ 1

Here ⟶ represents a morphism which directly corresponds to the arrows of the categorical diagrams

We use Lean’s OfNat.ofNat to tell the elaborator these numbers are actually objects in the category of circuits.

We’ll also use a primitve fork morphism that splits a wire to help connect our circuits:

abbrev fork :  (ofNat 1 : C) ⟶ 2

Proving theorems about a digital circuit

One way to prove properties about a circuit is by using what are known as denotational semantics. These semantics will denote the behaviour of circuits from their wiring to mathematical notation, in our case Lean4.

NOT

Let’s start by proving the denotational semantics of the not gate. Essentially, we want to say that not follows this truth table:

0 => 1
1 => 0

As a theorem we could state for any bit x a NOT gate returns !x, where ! is the NOT operator, which we can write in Lean as the following:

theorem not_def (x : Bool) : not.val #v[↑x] = #v[↑(!x)]

not_def, short for the definition of not, takes some bit, or Bool, x and returns a proposition that inputting x into not (not.val #v[↑x]) is equivalent to !x (#v[↑(!x)]).

.val is used to access the value of the Subtype ↑ is the coercion operator in Lean, we use it here to tell the elaborator to coerce the Bool bits to BelnapLevels (an implementation of the 4-value logic mentioned before.)

#v[...] is syntax to create a Vector, which is used here to represent groups of wires

We can prove this theorem by going through all cases of x and using reflection:

theorem not_def (x : Bool) : not.val #v[↑x] = #v[↑(!x)] := by cases x <;> rfl

XOR

First, let’s define some helper circuits to fork wires twice and copy pairs of bits:

def fork₂ : (ofNat 2 : CombinationalCircuit) ⟶ 4 := fork ⊗ₘ fork

⊗ₘ is the tensor morphism notation from mathlib

def copy : (ofNat 2 : CombinationalCircuit) ⟶ 4 := fork₂ ≫ (1 ◁ ((β_ 1 1).hom ▷ 1))

Now we can use copy with and, or, and not gates to define xor:

def xor : (ofNat 2 : CombinationalCircuit) ⟶ 1 := copy ≫ (and ⊗ₘ or) ≫ (not ⊗ₘ 𝟙 1) ≫ and

We can prove the semantics of xor in a similar way by going through all cases of both x and y:

theorem xor_def (x y : Bool) : xor.val #v[↑x, ↑y] = #v[↑((x && !y) || (!x && y))] := by
  cases x <;> cases y <;> rfl

Half-adder

An adder is comprised of two halfAdders, so we’ll have to define that first.

def halfAdder : (ofNat 2 : CombinationalCircuit) ⟶ 2 := copy ≫ (xor ⊗ₘ and)

theorem halfAdder_def
    (x y : Bool) :
    halfAdder.val #v[↑x, ↑y] = #v[↑((x && !y) || (!x && y)), ↑(x && y)] := by
  cases x <;> cases y <;> rfl

Adder

Now we’re finally ready for the full adder, which will use all our previous circuits in the form of two halfAdders and an or gate.

def adder : (ofNat 3 : CombinationalCircuit) ⟶ 2 :=
  (halfAdder ⊗ₘ 𝟙 1) ≫
  (1 ◁ (β_ 1 1).hom) ⊗≫
  (halfAdder ⊗ₘ 𝟙 1) ≫
  (𝟙 1 ⊗ₘ or)

Here we take advantage of ⊗≫ to have Lean’s elaborator automatically insert the required associator and whiskering, but it essentially just acts as composition.

theorem adder_def (x y z : Bool) :
    adder.val #v[↑x, ↑y, ↑z] =
      #v[↑((((x && !y) || (!x && y)) && !z) || (!(((x && !y) || (!x && y))) && z)),
         ↑((x && y) || (((x && !y) || (!x && y)) && z))] := by
  cases x <;> cases y <;> cases z <;> rfl

And that’s that! We’ve now verified the denotational semantics for the circuit of an adder. This same pattern of building up circuits from verifying them should naturally extend to much larger and complex real-world systems. If you’re interested in building your own circuits, please consider checking out circuitlib!

References

1. Ghica, D. R., Kaye, G., & Sprunger, D. (2025). A Complete Theory of Sequential Digital Circuits: Denotational, Operational and Algebraic Semantics. arXiv:2201.10456 ↩ ↩²

2. Belnap, N. D. (1977). A Useful Four-Valued Logic. Springer ↩ ↩²