Refinement types decorate the types of a programming language with logical predicates to allow more expressive type specifications. Originally, refinement type based specifications were restricted to SMT decidable theories and allowed automatic “light” verification, for example properties like non-division by zero or in-bound indexing. Verification of such light properties though requires “deeper” specifications, for example “is append associative?” or even “does your language preserve typing?” In this talk, I will present an overview of refinement types and using Liquid Haskell as the prototype refinement type implementation, will present various examples that cover both light and deep refinement type-based verification.