An overview of a formal model of the Pony language which allows us to prove Pony's guarantees about freedom from data-races while having more permissive definitions than the existing implementation. We also briefly discuss bugs found in the language implementation during development of the model.
