Refinement types doğrulama, bir tipin değerlerini sınırlayan mantıksal yüklemler ekleme fikrine dayanır. `{v : Int | v > 0}` gibi bir tip, yalnızca pozitif tam sayıları temsil eder; bu kısıtlama hem belgeleme hem de derleme zamanı garantisi olarak çalışır. Refinement types Liquid Haskell sistemi bu yaklaşımı Haskell'e entegre ederek SMT (Satisfiability Modulo Theories) çözücüler aracılığıyla doğrulamayı otomatikleştirir. Liquid Haskell'de bir fonksiyon şöyle imzalanabilir: `{-@ divide :: Int -> {v:Int | v /= 0} -> Int @-}`. Bu imza, ikinci argümanın sıfırdan farklı olmasını zorunlu kılar. Çağrı noktasında Liquid Haskell, argümanın bu koşulu sağladığını kanıtlamaya çalışır. Kanıtlanamıyorsa derleme hatası verilir. Refinement types Liquid Haskell bu süreci SMT çözücüye, genellikle Z3, devreder; kullanıcı manuel kanıt yazmak zorunda kalmaz. SMT tabanlı doğrulamanın güçlü yanı, lineer aritmetik, dizi teorisi ve eşitlik akıl yürütmesini otomatik olarak ele alabilmesidir. Örneğin bir dizinin indeksinin boyut sınırı içinde olduğunu doğrulamak, buffer overflow kanıtı, Liquid Haskell'in doğrudan çözebileceği bir SMT problemidir. Refinement types Liquid Haskell bu yolla bellek güvenliği özelliklerini statik olarak garanti altına alır. Sınırlılıklar da ciddidir. Nonlineer aritmetik, bitwise işlemler ve daha karmaşık yüklemler SMT çözücünün kapsamı dışına çıkabilir; bu durumda kullanıcı manuel hint veya assume-prove blokları sağlamak durumunda kalır. Ayrıca tür çıkarımı (inference) karmaşık veri yapılarında bazen yetersiz kalır ve kullanıcıdan ek anotasyon gerektirir. Praktik kullanım açısından Liquid Haskell, özellikle güvenlik açısından kritik kütüphanelerin doğrulanmasında değer görmüştür. Sıralı listenin sıralılık özelliğini, hash map'in boyut tutarlılığını veya şifreleme protokolünün durum geçişlerini refinement type'larla ifade etmek ve otomatik olarak doğrulatmak mümkündür. Dependent types ile karşılaştırıldığında refinement types Liquid Haskell daha kısıtlı ancak daha pratik bir uzay sunar: kullanıcı mevcut Haskell koduna ek anotasyonlar ekler, SMT otomatik kanıtlamayı üstlenir. Dependent types daha ifadelidir fakat her kanıtın elle yazılması gerekebilir. İkisi arasındaki seçim, doğrulamak istenen özelliğin karmaşıklığına ve ekibin teorik altyapısına bağlıdır.