Static type systems are integral to programming languages that utilize static typing. This integration is crucial because every valid program in these languages must pass type checking according to the defined type system. This process helps programmers identify and prevent many type errors at compile time, which could otherwise lead to runtime issues. Consequently, different formalisms are necessary to ensure a well-defined type system. The validity of these formalism relies on the rigorous verification of various properties within the type system. Unfortunately, this often involves applying axioms and inference rules to prove the absence of certain program behaviors, leaving many compiler developers and programmers with the daunting task of maintaining complex proofs. In this paper, we introduce a novel and practical method for describing a type system for any JVM-based language using set notation (including membership tests, subsets, sizes, and other properties), first-order logic, and type-specific grammar. We also detail the checkers we developed, outline the challenges we encountered, and share insights gained while describing aspects of the type system of Espresso, a subset of Java.