Concurrent revisions is a concurrency control model developed by Microsoft Research. It has many interesting properties that distinguish it from other well-known models such as transactional memory. One of these properties is determinacy: programs written within the model always produce the same outcome, independent of scheduling. The concurrent revisions model has an operational semantics, with an informal proof of determinacy. I formalized the semantics and the proof of determinacy in the proof assistant Isabelle/HOL. A number of subtle ambiguities in the specification of the semantics were identified, whose resolution required the semantics to be modified. I also found a simplification of the determinacy proof. While the uncovered issues do not appear to correspond to bugs in existing implementations, the formalization highlights some of the challenges that are involved in the general design and verification of concurrency control models.