You can implement pretty powerful type checkers as constraint based systems. I used Z3 in a project called LightDP to verify differential privacy as a property of the type system.