The RS-274/NGC standard provides an informal description of the command language implemented by computerized manufacturing devices like 3D printers and CNC machines. This language (RS-274/NGC) is often referred to as “G-code”. Although it was initially defined for conventional or subtractive manufacturing, a subset of the G-code commands have been adopted for additive manufacturing (AM) programs. Given the increasing importance of AM processes in manufacturing of critical components in system for transportation, medical, and other applications, verification of G-code programs is one approach to establish that these components meet their requirements. This paper describes a verified interpreter for the RS-274/NGC language. This verified interpreter provides a mechanized semantics for the command language, the state of the manufacturing device controller, a model of the physical state, and a correct by construction interpreter step function that evolves these states based on program commands. We also define verification condition checkers that the interpreter implements to check that a G-code program meets domain-specific correctness criteria related to its intended outcome. Our formalization is performed in Why3 and Rocq, and we use program extraction to OCaml to obtain an executable, verified interpreter. We also discuss our experiences with the initial subset of RS-274/NGC that we implemented and future directions to expand the breadth of RS-274/NGC that we can interpret along with more sophisticated domain-specific verification conditions.