A key piece of data in understanding mathematics from the perspective of model-based reasoning is the use of diagrams to discover and to convey mathematical concepts and proofs. A paradigmatic example of such use is found in the classical demonstrations of elementary Euclidean geometry. These are invariably presented with accompanying geometric diagrams. Great progress has been made recently with respect to the precise role the diagrams plays in the demonstrations, so much so that diagrammatic formalizations of elementary Euclidean geometry have been developed. The purpose of this chapter is to introduce these formalizations to those who seek to understand mathematics from the perspective of model-based reasoning.The formalizations are named FG and Eu. Both are based on insights articulated in Ken Manders' seminal analysis of Euclid's diagrammatic proofs. The chapter presents these insights, the challenges involved in realizing them in a formalization, and the way FG and Eu each meet these challenges. The chapter closes with a discussion of how the formalizations can each be thought to prespecify a species of model-based reasoning.