Phase transitions are ubiquitous in nature, ranging from protein folding and denaturisation, to the superconductor-insulator quantum phase transition, to the decoupling of forces in the early universe. Remarkably, phase transitions can be arranged into universality classes, where systems having unrelated microscopic physics exhibit identical scaling behaviour near the critical point. Here we present an experimental and theoretical study of the Bose-Einstein condensation phase transition of an atomic gas, focusing on one prominent universal element of phase transition dynamics: the spontaneous formation of topological defects during a quench through the transition. While the microscopic dynamics of defect formation in phase transitions are generally difficult to investigate, particularly for superfluid phase transitions, Bose-Einstein condensates (BECs) offer unique experimental and theoretical opportunities for probing such details. Although spontaneously formed vortices in the condensation transition have been previously predicted to occur, our results encompass the first experimental observations and statistical characterisation of spontaneous vortex formation in the condensation transition. Using microscopic theories that incorporate atomic interactions and quantum and thermal fluctuations of a finite-temperature Bose gas, we simulate condensation and observe vortex formation in close quantitative agreement with our experimental results. Our studies provide further understanding of the development of coherence in superfluids, and may allow for direct investigation of universal phase-transition dynamics. Published in: Nature 455, 948 (2008).