We show decidability of the satisfiability problem for an extension of the modal μ-calculus with event-recording clocks. Based on techniques for deciding the untimed μ-calculus, we present a complete set of reduction rules for constructing tableaux for formulas of this eventrecording logic. To keep track of the actual value of the clocks, the premises and conclusions of our tableau rules are augmented with timing contexts, which are sets of timing constraints satisfied by the actual value of the clocks. The decidability problem is shown to be EXPTIME complete. In addition, we address the problem of model synthesis, that is, given a formula φ, we construct an event-recording automaton that satisfies φ.