We present an equational verification of Milner's scheduler, which we checked by computer. To our knowledge, this is the first time that the scheduler is proof-checked for a general number n of scheduled processes.
The work of the first author took place in the context of EC Basic Research Action 7166 concur 2. The work of the second author is supported by the Netherlands Computer Science Research Foundation (SION) with financial support of the Netherlands Organisation for Scientific Research (NWO).