  An event structure is a mathematical abstraction modeling concepts as
causality, conflict and concurrency between events. While many other
mathematical structures, including groups, topological spaces, rings, abound
with algorithms and formulas to generate, enumerate and count particular sets
of their members, no algorithm or formulas are known to generate or count all
the possible event structures over a finite set of events. We present an
algorithm to generate such a family, along with a functional implementation
verified using Isabelle/HOL. As byproducts, we obtain a verified enumeration of
all possible preorders and partial orders. While the integer sequences counting
preorders and partial orders are already listed on OEIS (On-line Encyclopedia
of Integer Sequences), the one counting event structures is not. We therefore
used our algorithm to submit a formally verified addition, which has been
successfully reviewed and is now part of the OEIS.
