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.

Thank you for your explanation and writing this. Added in my todo list to play with. I understand this one is the official repo: https://github.com/ucsd-progsys/liquidhaskell ?

While you can write verified programs in agda, and use the MAlonzo FFI to extract haskell code, the generated code is very inefficient. On the other hand, this lets you write proofs in Haskell that coexist with your program, so there's little to no impact on runtime performance.

Also, Agda is an implementation of Martin-Lof type theory, which is very, very different from what SMT is.