It’s the process of verifying the type safety of a program based on analysis of the program’s source code.