We show decidability of the satisfiability problem for an extension of the modal mu-calculus with event-recording clocks. Based on techniques for deciding the untimed mu-calculus, we present a complete set of reduction rules for constructing tableaux for formulas of this event-recording 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. In addition, we address the problem of model synthesis, that is, given a formula phi, we construct an event-recording automaton that satisfies phi. The decidability problem is shown to be EXPSPACE-complete.