Most type systems are based on the style of over-approximate or “may-style” reasoning found in Hoare logic and are used to show that something does not happen. This paper develops an alternative type system based on the under-approximate or “must-style” reasoning found in incorrectness logic in order to show that something does happen.
This type system is used to show that a random test generator is theoretically able to generate all possible values of an abstract data type.
One minor point to note (I’m not sure if the paper mentions this) is that, if you are using an ADT to represent abstract syntax trees, then you usually don’t want to generate ASTs that represent illegal programs (e.g., containing type errors or references to undeclared variables).