This paper examines von Neumann-Bernays-Gödel (NBG) axiomatic set theory’s development and formalization. We trace NBG’s evolution through von Neumann’s introduction of class concepts, Bernays’ refinements, and Gödel’s finitely axiomatizable system, highlighting his innovative “Existence Axioms of Classes” that distinguish NBG from ZFC and MK theories. We present NBG’s formalization in Coq, encoding its types, axioms, and theorems. Comparing with ZFC and MK demonstrates NBG’s advantages in addressing set theory paradoxes through classes, proven by showing “Russell’s class is not a set.” This work provides a framework for mechanical verification of set-theoretical foundations and perspectives on relationships between axiomatic systems. Future directions include extending these techniques to other systems and identifying optimal axiomatizations for specific domains. NBG’s continuing relevance suggests ongoing applications where proper class treatment and simplicity offer advantages.