[Aurel300]

The two tools address similar problems. The kinds of properties you can prove (automatically) should also be similar, because both Prusti and Liquid Haskell ultimately use an SMT solver to check if assertions hold.

From what I have seen LH focuses on integrating into the type system (it is Liquid as in the 2008 Liquid Types paper). Generally it is possible to rewrite properties attached to a type to contracts, e.g. a non-zero Int input becomes a precondition that says that argument is non-zero. Checking termination with Prusti is also something we are working on.