diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+# 0.1.1.0
+
+* Add liquid haskell refinements.
+
 # 0.0.1.0
 
 * Initial release
diff --git a/grow-vector.cabal b/grow-vector.cabal
--- a/grow-vector.cabal
+++ b/grow-vector.cabal
@@ -1,7 +1,7 @@
 name:                grow-vector
 synopsis:            Mutable vector with efficient appends
 description:         Mutable vector with efficient updates. Simple implementation on partially filled array with capacity tracking and resizing.
-version:             0.1.0.0
+version:             0.1.1.0
 license:             MIT
 license-file:        LICENSE
 copyright:           2020 Anton Gushcha
@@ -12,6 +12,7 @@
 extra-source-files:
   README.md
   CHANGELOG.md
+data-files:           src/Data/Vector/Grow/Unboxed.spec
 
 source-repository head
   type: git
@@ -36,6 +37,7 @@
         liquid-base
       , liquid-vector
       , liquidhaskell >= 0.8.10
+    cpp-options: -DLIQUID
   else
     build-depends:
         base          >= 4.5      && < 4.15
diff --git a/src/Data/Vector/Grow/Unboxed.hs b/src/Data/Vector/Grow/Unboxed.hs
--- a/src/Data/Vector/Grow/Unboxed.hs
+++ b/src/Data/Vector/Grow/Unboxed.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -65,18 +66,18 @@
 -- | Return current capacity of the vector (amount of elements that it can fit without realloc)
 capacity :: (Unbox a, PrimMonad m) => GrowVector (PrimState m) a -> m Int
 capacity v = do
-  mv <- readMutVar . growVector $! v
+  mv <- readMutVar $ growVector v
   pure $ M.length mv
 {-# INLINE capacity #-}
 
 -- | Return current amount of elements in the vector
 length :: (Unbox a, PrimMonad m) => GrowVector (PrimState m) a -> m Int
-length = readMutVar . growVectorLength
+length v = readMutVar $ growVectorLength v
 {-# INLINE length #-}
 
 -- | Return 'True' if there is no elements inside the vector
 null :: (Unbox a, PrimMonad m) => GrowVector (PrimState m) a -> m Bool
-null = fmap (== 0) . length
+null v = fmap (== 0) $ length v
 {-# INLINE null #-}
 
 -- | Allocation of new growable vector with given capacity.
@@ -98,7 +99,7 @@
   -> m (GrowVector (PrimState m) a)
 slice i n v = do
   newSize <- newMutVar n
-  mv <- readMutVar . growVector $! v
+  mv <- readMutVar $ growVector v
   newVec <- newMutVar $! M.slice i n mv
   pure $! GrowVector newVec newSize
 {-# INLINABLE slice #-}
@@ -117,13 +118,14 @@
 -- | Freezing growable vector. It will contain only actual elements of the vector not including capacity
 -- space, but you should call 'U.force' on resulting vector to not hold the allocated capacity of original
 -- vector in memory.
+
 freeze :: (Unbox a, PrimMonad m)
   => GrowVector (PrimState m) a
   -> m (U.Vector a)
 freeze v = do
   n <- length v
-  mv <- readMutVar . growVector $! v
-  U.freeze . M.take n $! mv
+  mv <- readMutVar $ growVector v
+  U.freeze $ M.take n mv
 {-# INLINABLE freeze #-}
 
 -- | Ensure that grow vector has at least given capacity possibly with reallocation.
@@ -134,19 +136,19 @@
 ensure v n = do
   c <- capacity v
   unless (c >= n) $ do
-    mv <- readMutVar . growVector $! v
+    mv <- readMutVar $ growVector v
     writeMutVar (growVector v) =<< M.grow mv (n - c)
 {-# INLINABLE ensure #-}
 
 -- | Ensure that grow vector has enough space for additonal n elements.
--- We grow vector by 1.5 factor or by
+-- We grow vector by 1.5 factor or by required elements count * 1.5.
 ensureAppend :: (Unbox a, PrimMonad m)
   => GrowVector (PrimState m) a
   -> Int -- ^ Additional n elements
   -> m ()
 ensureAppend v i = do
-  n <- readMutVar . growVectorLength $! v
-  mv <- readMutVar . growVector $! v
+  n <- readMutVar $ growVectorLength v
+  mv <- readMutVar $ growVector v
   let c = M.length mv
   unless (c >= n + i) $ do
     let growFactor = 1.5
@@ -160,9 +162,11 @@
   -> Int -- ^ Index of element. Must be in [0 .. length) range
   -> m a
 read v i = do
-  n <- readMutVar . growVectorLength $! v
+  n <- readMutVar $ growVectorLength v
+#ifndef LIQUID
   when (i < 0 || i >= n) $ error $ "GrowVector.read: index " <> show i <> " is out bounds " <> show n
-  mv <- readMutVar . growVector $! v
+#endif
+  mv <- readMutVar $ growVector v
   M.unsafeRead mv i
 {-# INLINABLE read #-}
 
@@ -172,7 +176,7 @@
   -> Int -- ^ Index of element. Must be in [0 .. length) range
   -> m a
 unsafeRead v i = do
-  mv <- readMutVar . growVector $! v
+  mv <- readMutVar $ growVector v
   M.unsafeRead mv i
 {-# INLINABLE unsafeRead #-}
 
@@ -183,9 +187,11 @@
   -> a
   -> m ()
 write v i a = do
-  n <- readMutVar . growVectorLength $! v
+  n <- readMutVar $ growVectorLength v
+#ifndef LIQUID
   when (i < 0 || i >= n) $ error $ "GrowVector.write: index " <> show i <> " is out bounds " <> show n
-  mv <- readMutVar . growVector $! v
+#endif
+  mv <- readMutVar $ growVector v
   M.unsafeWrite mv i a
 {-# INLINABLE write #-}
 
@@ -196,7 +202,7 @@
   -> a
   -> m ()
 unsafeWrite v i a = do
-  mv <- readMutVar . growVector $! v
+  mv <- readMutVar $ growVector v
   M.unsafeWrite mv i a
 {-# INLINABLE unsafeWrite #-}
 
@@ -217,8 +223,8 @@
   -> a
   -> m ()
 unsafePushBack v a = do
-  n <- readMutVar . growVectorLength $! v
-  mv <- readMutVar . growVector $! v
+  n <- readMutVar $ growVectorLength v
+  mv <- readMutVar $ growVector v
   M.write mv n a
   writeMutVar (growVectorLength v) (n+1)
 {-# INLINABLE unsafePushBack #-}
diff --git a/src/Data/Vector/Grow/Unboxed.spec b/src/Data/Vector/Grow/Unboxed.spec
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Grow/Unboxed.spec
@@ -0,0 +1,89 @@
+module spec Data.Vector.Grow.Unboxed where
+
+import Data.Vector
+
+measure vlen    :: forall a. (U.Vector a) -> Int
+
+invariant       {v: U.Vector a | 0 <= vlen v }
+
+(U.!)           :: forall a. x:(U.Vector a) -> vec:{v:Nat | v < vlen x } -> a
+
+U.unsafeIndex :: forall a. x:(U.Vector a) -> vec:{v:Nat | v < vlen x } -> a
+
+U.fromList  :: forall a. x:[a] -> {v: U.Vector a  | vlen v = len x }
+
+U.length    :: forall a. x:(U.Vector a) -> {v : Nat | v = vlen x }
+
+U.replicate :: n:Nat -> a -> {v:U.Vector a | vlen v = n}
+
+U.imap :: (Nat -> a -> b) -> x:(U.Vector a) -> {y:U.Vector b | vlen y = vlen x }
+
+U.map :: (a -> b) -> x:(U.Vector a) -> {y:U.Vector b | vlen y = vlen x }
+
+U.head :: forall a. {xs: U.Vector a | vlen xs > 0} -> a
+
+
+measure gvlen :: GrowVector s a -> Int
+measure gvcap :: GrowVector s a -> Int
+
+invariant {v: GrowVector s a | 0 <= gvlen v }
+invariant {v: GrowVector s a | 0 <= gvcap v }
+invariant {v: GrowVector s a | gvlen v <= gvcap v }
+
+type GrowVectorN s a N = {v:GrowVector s a | gvlen v == N}
+type GrowVectorC s a C = {v:GrowVector s a | gvcap v == C}
+type GrowVectorNC s a N C = {v:GrowVector s a | gvlen v == N && gvcap v == C}
+
+assume capacity :: (Unbox a, PrimMonad m) => x : GrowVector (PrimState m) a -> m {v:Int | v = gvcap x}
+
+assume length :: (Unbox a, PrimMonad m) => x : GrowVector (PrimState m) a -> m {v:Int | v = gvlen x}
+
+null :: (Unbox a, PrimMonad m) => x : GrowVector (PrimState m) a -> m { v:Bool | v <=> gvlen x = 0}
+
+assume newSized :: (Unbox a, PrimMonad m) => l:Nat -> {c:Nat | c >= l} -> m { v:(GrowVector (PrimState m) a) | l = gvlen v && c = gvcap v }
+
+assume slice :: (Unbox a, PrimMonad m)
+  => i:Nat
+  -> n:Nat
+  -> {x:(GrowVector (PrimState m) a) | i < gvlen x && i + n <= gvlen x }
+  -> m {y:(GrowVector (PrimState m) a) | gvlen y = n && gvcap y = n }
+
+assume thaw :: (Unbox a, PrimMonad m)
+  => v : U.Vector a
+  -> m {gv:(GrowVector (PrimState m) a) | vlen v == gvlen gv && gvcap gv == 0 }
+
+freeze :: (Unbox a, PrimMonad m)
+  => gv : GrowVector (PrimState m) a
+  -> m {v:(U.Vector a) | vlen v == gvlen gv }
+
+assume ensure :: (Unbox a, PrimMonad m)
+  => x : GrowVector (PrimState m) a
+  -> c : Nat
+  -> m {r:() | gvcap x = c}
+
+assume ensureAppend :: (Unbox a, PrimMonad m)
+  => x : GrowVector (PrimState m) a
+  -> n : Nat
+  -> m {r:() | gvcap x >= gvlen x + n }
+
+read :: (Unbox a, PrimMonad m)
+  => x : GrowVector (PrimState m) a
+  -> {i:Nat | i < gvlen x}
+  -> m a
+
+unsafeRead :: (Unbox a, PrimMonad m)
+  => x : GrowVector (PrimState m) a
+  -> {i:Nat | i < gvlen x}
+  -> m a
+
+write :: (Unbox a, PrimMonad m)
+  => x : GrowVector (PrimState m) a
+  -> {i:Nat | i < gvlen x}
+  -> a
+  -> m ()
+
+unsafeWrite :: (Unbox a, PrimMonad m)
+  => x : GrowVector (PrimState m) a
+  -> {i:Nat | i < gvlen x}
+  -> a
+  -> m ()