Python’s typing system has evolved pragmatically into a powerful but theoretically fragmented system, with scattered specifications. This paper proposes a formalization to address this fragmentation. The central contribution is a formal foundation that uses existential types to elegantly describe Python’s type system. This work aims to serve as a fundamental first step towards the future development of type inference tools.