In 2010, Iago Abal wrote this specification of Darcs' patch theory kernel in Alloy as course work for the Formal Methods for Software Engineering course at University of Minho. By patch theory kernel, we mean the set of primitive patches and associated operations. This formalization does not model merges.