Liquid Types use the SMT solver to automatically generate proofs, while in Agda the user needs to manually specify the proofs. Also, Agda is a verification spec

Liquid Types use the SMT solver to automatically generate proofs, while in Agda the user needs to manually specify the proofs. Also, Agda is a verification specific language, while (Liquid) Haskell is a general purpose language, which means that with Liquid Haskell your verified code can use general language features, such as exceptions, diverging code, parallelism and all the Haskell optimized libraries.