Phase transitions are ubiquitous in nature, and can be arranged into universality classes such that systems having unrelated microscopic physics show identical scaling behaviour near the critical point. One prominent universal element of many continuous phase transitions is the spontaneous formation of topological defects during a quench through the critical point. The microscopic dynamics of defect formation in such transitions are generally difficult to investigate, particularly for superfluids. However, Bose-Einstein condensates (BECs) offer unique experimental and theoretical opportunities for probing these details. Here we present an experimental and theoretical study of the BEC phase transition of a trapped atomic gas, in which we observe and statistically characterize the spontaneous formation of vortices during condensation. 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.