Logical clocks are a family of techniques for tracking causal relationships between concurrent events. Logical clocks underpin causal message delivery protocols, data race checking tools, and conflict resolution schemes for concurrent writes. We develop a mechanization of the theory of logical clocks in Agda, including a generic proof of monotonicity (Lamport’s “clock condition”) that can be instantiated on any clock. To achieve this, we model executions with a surface syntax inspired by Lamport-style execution diagrams, and interpret executions against any chosen clock semantics. We expect our approach to generalize to any replicated data structure with an idempotent join operator and inflationary updates, including CRDTs and LVars, and hope to generalize further to non-idempotent settings modeled by arbitrary partial commutative monoids (PCMs).