diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,7 +8,19 @@
 
 ## Unreleased
 
-## 0.4.0.0 - 2026-03-16 
+## 0.4.0.1 - 2026-03-17
+
+### Added
+- Optional `liquid` Cabal flag (`--flag haal:liquid`) to enable LiquidHaskell
+  verification without requiring it as a dependency for normal builds.
+
+### Verified
+- `Haal.BlackBox`: `walk` produces outputs of length equal to the input length.
+- `Haal.Learning.LMstar`: `ObservationTable` invariant that all entries in
+  `mappingT` map to non-empty output lists, preserved across `updateMap`,
+  `makeConsistent`, `makeClosed`, and `initializeOT`.
+
+## 0.4.0.0 - 2026-03-16
 
 ### Changed 
 - Changed the types of oracles' constructors from `<Oracle>` to `Either String <Oracle>`
diff --git a/haal.cabal b/haal.cabal
--- a/haal.cabal
+++ b/haal.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           haal
-version:        0.4.0.0
+version:        0.4.0.1
 synopsis:       A Haskell library for Active Automata Learning.
 description:    Please see the README on GitHub at <https://github.com/steve-anunknown/haal#readme>
 category:       Model Learning
@@ -26,6 +26,11 @@
   type: git
   location: https://github.com/steve-anunknown/haal
 
+flag liquid
+  description: Enable LiquidHaskell verification
+  manual: True
+  default: False
+
 library
   exposed-modules:
       Haal.Automaton.DFA
@@ -47,12 +52,16 @@
       src
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
   build-depends:
-      base >=4.18.3 && <4.21
-    , containers ==0.6.*
+      base >=4.18.3 && <4.19
+    , containers >=0.6.7 && <0.7
     , mtl >=2.3.1 && <2.4
-    , random ==1.2.1.*
-    , vector ==0.13.1.*
+    , random >=1.3.1 && <1.4
+    , vector >=0.13.2 && <0.14
   default-language: Haskell2010
+  if flag(liquid)
+    cpp-options: -DLIQUID
+    build-depends:
+        liquidhaskell
 
 executable demo
   main-is: demo.hs
@@ -65,7 +74,7 @@
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
   build-depends:
       base
-    , containers ==0.6.*
+    , containers
     , haal
   default-language: Haskell2010
 
@@ -81,7 +90,7 @@
   build-depends:
       base
     , haal
-    , mtl >=2.3.1 && <2.4
+    , mtl
   default-language: Haskell2010
 
 executable io
@@ -96,8 +105,8 @@
   build-depends:
       base
     , haal
-    , mtl >=2.3.1 && <2.4
-    , process >=1.6.19 && <1.6.25
+    , mtl
+    , process >=1.6.19 && <1.7
   default-language: Haskell2010
 
 executable website
@@ -112,7 +121,7 @@
   build-depends:
       base
     , haal
-    , process >=1.6.19 && <1.6.25
+    , process >=1.6.19 && <1.7
   default-language: Haskell2010
 
 test-suite haal-test
@@ -130,10 +139,10 @@
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       QuickCheck
-    , base >=4.18.3 && <4.21
-    , containers ==0.6.*
+    , base >=4.18.3 && <4.19
+    , containers
     , haal
     , hspec
-    , mtl >=2.3.1 && <2.4
-    , random ==1.2.1.*
+    , mtl
+    , random
   default-language: Haskell2010
diff --git a/src/Haal/BlackBox.hs b/src/Haal/BlackBox.hs
--- a/src/Haal/BlackBox.hs
+++ b/src/Haal/BlackBox.hs
@@ -1,7 +1,13 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+#ifdef LIQUID
+{-# OPTIONS_GHC -fplugin=LiquidHaskell
+                -fplugin-opt=LiquidHaskell:--prune-unsorted
+                -fplugin-opt=LiquidHaskell:--no-termination #-}
+#endif
 
 {- | This module defines the BlackBox type class as well as the Automaton and SUL
 sub classes.
@@ -50,12 +56,15 @@
 
 -- | Finite is an alias for (Enum, Bounded).
 type Finite i = (Enum i, Bounded i)
+
 -- | FiniteEq is an alias for (Eq, Finite).
 type FiniteEq i = (Eq i, Finite i)
+
 -- | FiniteOrd is an alias for (Ord, Bounded).
 type FiniteOrd i = (Ord i, Finite i)
 
 -- | Generalization of 'step' that operates on a list of inputs.
+{-@ walk :: (SUL sul m) => sul i o -> xs:[i] -> m (sul i o, {ys:[o] | len ys == len xs}) @-}
 walk :: (SUL sul m) => sul i o -> [i] -> m (sul i o, [o])
 walk sul [] = pure (sul, [])
 walk sul (x : xs) = do
@@ -63,13 +72,25 @@
     (sul'', os) <- walk sul' xs
     pure (sul'', o : os)
 
+{-@ rangeIN :: (Enum i, Bounded i) => sul i o -> {is:[i] | len is > 0} @-}
+rangeIN :: (Finite i) => sul i o -> [i]
+rangeIN _ = minBound : [succ minBound .. maxBound]
+
+{-@ rangeOUT :: (Enum o, Bounded o) => sul i o -> {os:[o] | len os > 0} @-}
+rangeOUT :: (Finite o) => sul i o -> [o]
+rangeOUT _ = minBound : [succ minBound .. maxBound]
+
+{-@ assume Set.fromList :: Ord a => xs:[a] -> {s:Set.Set a | len xs > 0 => Set.size s > 0} @-}
+
 -- | Return a Set containing only the valid inputs of the SUL.
+{-@ inputs :: (Ord i, Enum i, Bounded i) => sul i o -> {is:Set.Set i | Set.size is > 0} @-}
 inputs :: (FiniteOrd i) => sul i o -> Set.Set i
-inputs _ = Set.fromList [minBound .. maxBound]
+inputs x = Set.fromList $ rangeIN x
 
 -- | Return a Set containing only the valid outputs of the SUL.
+{-@ outputs :: (Ord o, Enum o, Bounded o) => sul i o -> {os:Set.Set o | Set.size os > 0} @-}
 outputs :: (FiniteOrd o) => sul i o -> Set.Set o
-outputs _ = Set.fromList [minBound .. maxBound]
+outputs x = Set.fromList $ rangeOUT x
 
 {- | The 'Automaton' type class extends the 'SUL' type class and adds
 support for automata operations. Automatons are models, not programs,
diff --git a/src/Haal/EquivalenceOracle/RandomWalk.hs b/src/Haal/EquivalenceOracle/RandomWalk.hs
--- a/src/Haal/EquivalenceOracle/RandomWalk.hs
+++ b/src/Haal/EquivalenceOracle/RandomWalk.hs
@@ -12,7 +12,7 @@
 import Haal.Experiment
 import System.Random (
     Random (randomR, randomRs),
-    RandomGen (split),
+    SplitGen (splitGen),
     StdGen,
  )
 
@@ -36,7 +36,7 @@
 -- | Generates a random walk for the automaton.
 randomWalkSuite :: (FiniteOrd a) => RandomWalk -> sul a o -> (RandomWalk, [[a]])
 randomWalkSuite (RandomWalk (RandomWalkConfig{rwlGen = g, rwlMaxSteps = maxS, rwlRestart = restartP})) aut =
-    let (g1, g2) = split g
+    let (g1, g2) = splitGen g
         alphabet = V.fromList . Set.toList $ inputs aut
         randomInputs = take maxS $ randomRs (0, V.length alphabet - 1) g1
         inputSequence = map (alphabet V.!) randomInputs
diff --git a/src/Haal/Learning/LMstar.hs b/src/Haal/Learning/LMstar.hs
--- a/src/Haal/Learning/LMstar.hs
+++ b/src/Haal/Learning/LMstar.hs
@@ -1,19 +1,27 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
+#ifdef LIQUID
+{-# OPTIONS_GHC -fplugin=LiquidHaskell
+                -fplugin-opt=LiquidHaskell:--prune-unsorted
+                -fplugin-opt=LiquidHaskell:--no-termination #-}
+#endif
 
 -- | This module implements the LM* algorithm for learning Mealy automata.
 module Haal.Learning.LMstar (
     lmstar,
     LMstar,
+    LMstarState (..),
     LMstarConfig (..),
     mkLMstar,
 )
 where
 
-import Control.Monad (foldM, forM)
+import Control.Monad (foldM)
 import Control.Monad.Reader (MonadReader (ask), MonadTrans (lift))
+import Data.Foldable (find)
 import qualified Data.List as List
 import qualified Data.Map as Map
 import qualified Data.Maybe as Maybe
@@ -22,30 +30,80 @@
 import Haal.BlackBox
 import Haal.Experiment
 
+{-@ ignore otRefinePlus @-}
+{-@ ignore otRefineAngluin @-}
+{-@ ignore lmstar @-}
+
+{-@ die :: {v:String | false} -> a @-}
+die :: String -> a
+die = error
+
+{-@ headLH :: {v:[a] | len v > 0} -> a @-}
+headLH :: [a] -> a
+headLH [] = die "impossible: headLH called with empty list"
+headLH (x : _) = x
+
+{-@ dropLH :: xs:[a] -> {v:Int | 0 <= v && v < len xs} -> {r:[a] | len r = len xs - v} @-}
+dropLH :: [a] -> Int -> [a]
+dropLH list number
+    | number >= length list = die "impossible: dropLH called with number larger than list length"
+    | otherwise = drop number list
+
 -- | The 'ObservationTable' type is a data type for storing the observation table of the LM* algorithm.
+
+{-@ data ObservationTable i o = ObservationTable
+    { prefixSetS  :: Set.Set [i]
+    , suffixSetE  :: Set.Set {v:[i] | len v > 0}
+    , mappingT    :: Map.Map ([i], [i]) {v:[o] | len v > 0}
+    , prefixSetSI :: Set.Set {v:[i] | len v > 0}
+    } @-}
 data ObservationTable i o = ObservationTable
     { prefixSetS :: Set.Set [i]
+    -- ^ sm = prefix closed set over @i@
     , suffixSetE :: Set.Set [i]
-    , mappingT :: Map.Map ([i], [i]) o
-    , -- more fields to avoid recomputing
-      prefixSetSI :: Set.Set [i]
+    -- ^ em = suffix closed set over @i@, excluding the empty word
+    , mappingT :: Map.Map ([i], [i]) [o]
+    -- ^ tm = finite mapping from (sm U (sm * I)) X em -> @o@+
+    , prefixSetSI :: Set.Set [i]
+    -- ^ sm * I = one-symbol extension of sm
     }
     deriving (Show)
 
+{-@ assume Set.difference :: forall <p :: a -> Bool>.
+     Ord a => Set.Set (a<p>) -> Set.Set a -> Set.Set (a<p>)
+@-}
+{-@ assume Set.cartesianProduct :: forall <p1 :: a -> Bool, p2 :: b -> Bool>.
+     (Ord a, Ord b) => Set.Set (a<p1>) -> Set.Set (b<p2>) -> Set.Set (a<p1>, b<p2>)
+@-}
+
 {- | The 'LMstarConfig' type is a configuration type for the LM* algorithm.
 It allows the user to choose between the original LM* algorithm and the LM+ algorithm.
 -}
 data LMstarConfig = Star | Plus
 
--- | The 'LMstar' type is a wrapper around the 'ObservationTable' type and represents the LM* algorithm.
-data LMstar i o = LMstar (ObservationTable i o) | LMplus (ObservationTable i o)
+-- | The 'LMstarState' type tracks whether the observation table has been initialized.
+data LMstarState i o = Uninit | Init (ObservationTable i o)
+    deriving (Show)
 
-{- | The 'mkLMstar' function creates a new instance of the 'LMstar' type. It holds a dummy value
-so that the user does not have to provide an initial observation table.
--}
+{-@ measure _isUninit @-}
+_isUninit :: LMstarState i o -> Bool
+_isUninit Uninit = True
+_isUninit _ = False
+
+{-@ measure _lmState @-}
+_lmState :: LMstar i o -> LMstarState i o
+_lmState (LMstar s) = s
+_lmState (LMplus s) = s
+
+-- | The 'LMstar' type wraps an 'LMstarState' and represents the LM* algorithm.
+data LMstar i o = LMstar (LMstarState i o) | LMplus (LMstarState i o)
+
+-- | The 'mkLMstar' function creates a new uninitialized instance of the 'LMstar' type.
+
+{-@ mkLMstar :: LMstarConfig -> {v:LMstar i o | _isUninit (_lmState v)} @-}
 mkLMstar :: LMstarConfig -> LMstar i o
-mkLMstar Star = LMstar (error "this is invisible")
-mkLMstar Plus = LMplus (error "this is invisible")
+mkLMstar Star = LMstar Uninit
+mkLMstar Plus = LMplus Uninit
 
 -- | The 'equivalentRows' function checks if two rows in the observation table are equivalent.
 equivalentRows :: forall i o. (Ord i, Eq o) => ObservationTable i o -> [i] -> [i] -> Bool
@@ -63,18 +121,17 @@
     ExperimentT (sul i o) m (ObservationTable i o)
 initializeOT = do
     sul <- ask
-    let alph = List.map (: []) $ Set.toList $ inputs sul
+    let
+        alph = List.map (: []) $ Set.toList $ inputs sul
         sm = Set.singleton []
+        {-@ sm_I :: Set.Set {v:[i] | len v = 1} @-}
         sm_I = Set.fromList alph
+        {-@ em :: Set.Set {v:[i] | len v = 1} @-}
         em = Set.fromList alph
-        domain = Set.toList $ (sm `Set.union` sm_I) `Set.cartesianProduct` em
-    -- monadic mapping because walk is in m
-    tmList <- forM domain $ \(in1, in2) -> do
-        sul0 <- lift $ reset sul
-        (_, outs) <- lift $ walk sul0 (in1 ++ in2)
-        pure ((in1, in2), last outs)
-
-    let tm = Map.fromList tmList
+        {-@ domain :: Set.Set ([i], {v:[i] | len v = 1}) @-}
+        domain = (sm `Set.union` sm_I) `Set.cartesianProduct` em
+    sulR <- lift $ reset sul
+    tm <- lift $ updateMap Map.empty domain sulR
 
     return
         ( ObservationTable
@@ -86,6 +143,8 @@
         )
 
 -- | The 'equivalenceClasses' function computes the equivalence classes of the observation table.
+
+{-@ equivalenceClasses :: (FiniteOrd i, Eq o) => ObservationTable i o -> Map.Map [i] [[i]] @-}
 equivalenceClasses ::
     forall i o.
     (FiniteOrd i, Eq o) =>
@@ -109,51 +168,72 @@
     (SUL sul m, FiniteOrd i, Eq o, Monad m) =>
     LMstar i o ->
     ExperimentT (sul i o) m (LMstar i o, MealyAutomaton StateID i o)
-lmstar (LMstar ot) = case otIsClosed ot of
+lmstar (LMstar (Init ot)) = case otIsClosed ot of
     [] -> case otIsConsistent ot of
         ([], []) -> case makeHypothesis ot of
-            Just hyp -> return (LMstar ot, hyp)
-            Nothing -> error "LM*: invariant violation — makeHypothesis failed on closed consistent table"
+            Just hyp -> return (LMstar (Init ot), hyp)
+            Nothing -> die "LM*: invariant violation — makeHypothesis failed on closed consistent table"
         inc' -> do
             ot' <- makeConsistent ot inc'
-            lmstar (LMstar ot')
+            lmstar (LMstar (Init ot'))
     inc -> do
         ot' <- makeClosed ot inc
-        lmstar (LMstar ot')
-lmstar (LMplus ot) = case otIsClosed ot of
+        lmstar (LMstar (Init ot'))
+lmstar (LMplus (Init ot)) = case otIsClosed ot of
     [] -> case makeHypothesis ot of
-        Just hyp -> return (LMplus ot, hyp)
-        Nothing -> error "LM+: invariant violation — makeHypothesis failed on closed table"
+        Just hyp -> return (LMplus (Init ot), hyp)
+        Nothing -> die "LM+: invariant violation — makeHypothesis failed on closed table"
     inc -> do
         ot' <- makeClosed ot inc
-        lmstar (LMplus ot')
+        lmstar (LMplus (Init ot'))
+lmstar (LMstar Uninit) = die "lmstar called before initialize"
+lmstar (LMplus Uninit) = die "lmstar called before initialize"
 
--- | The 'otIsClosed' function checks if the observation table is closed.
+{- | The 'otIsClosed' function checks if the observation table is closed.
+The observation table is closed if every prefix of `prefixSetSI` belongs
+to the same equivalence class as some prefix of `prefixSetS`. If the observation
+table is closed, it returns an empty list, whereas if it is not, it returns the
+problematic prefix from `prefixSetSI` that does not have the same equivalence class
+as any prefix from `prefixSetS`.
+-}
 otIsClosed :: forall i o. (FiniteOrd i, Eq o) => ObservationTable i o -> [i]
 otIsClosed ot = Maybe.fromMaybe [] exists
   where
     sm = prefixSetS ot
     sm_I = prefixSetSI ot
 
-    exists = List.find (\x -> not $ any (equivalentRows ot x) sm) sm_I
+    exists = find (\x -> not $ any (equivalentRows ot x) sm) sm_I
 
--- | The 'otIsConsistent' function checks if the observation table is consistent.
+{- | The 'otIsConsistent' function checks if the observation table is consistent.
+Returns @([], [])@ if consistent, otherwise returns @([a], e)@ where @a@ is the
+distinguishing letter and @e@ is an existing suffix witnessing the inconsistency,
+so that @[a] ++ e@ can be added to E.
+-}
 otIsConsistent :: forall i o. (FiniteOrd i, Eq o) => ObservationTable i o -> ([i], [i])
 otIsConsistent ot = Maybe.fromMaybe ([], []) condition
   where
     alph = [minBound .. maxBound] :: [i]
     sm = Set.toList $ prefixSetS ot
+    em = Set.toList $ suffixSetE ot
 
-    equivalentPairs = [(r1, r2) | r1 <- sm, r2 <- sm, r1 /= r2, equivalentRows ot r1 r2]
+    equivalentPairs = [(r1, r2) | r1 <- sm, r2 <- sm, r1 <= r2, equivalentRows ot r1 r2]
 
-    condition =
-        List.find
-            ( \(a, b) ->
-                any
-                    (\x -> not (equivalentRows ot (a ++ [x]) (b ++ [x])))
-                    alph
-            )
-            equivalentPairs
+    condition = do
+        (s1, s2) <-
+            find
+                ( \(s1, s2) ->
+                    any (\x -> not (equivalentRows ot (s1 ++ [x]) (s2 ++ [x]))) alph
+                )
+                equivalentPairs
+        x <-
+            find
+                (\x -> not (equivalentRows ot (s1 ++ [x]) (s2 ++ [x])))
+                alph
+        e <-
+            find
+                (\e -> Map.lookup (s1 ++ [x], e) (mappingT ot) /= Map.lookup (s2 ++ [x], e) (mappingT ot))
+                em
+        return ([x], e)
 
 -- | The 'otRefineAngluin' function refines the observation table based on a counterexample, according to Angluin's algorithm.
 otRefineAngluin ::
@@ -182,6 +262,8 @@
 the default 'StateID' type defined in the 'Experiment' module for representing the automaton states.
 Returns 'Nothing' if the observation table is malformed (invariant violated).
 -}
+
+{-@ makeHypothesis :: (FiniteOrd i, Eq o) => ObservationTable i o -> Maybe (MealyAutomaton StateID i o) @-}
 makeHypothesis :: forall i o. (FiniteOrd i, Eq o) => ObservationTable i o -> Maybe (MealyAutomaton StateID i o)
 makeHypothesis ot = do
     startId <- getStateId []
@@ -198,15 +280,14 @@
     repList = Map.keys equivMap
     numStates = length repList
     repToId = Map.fromList (zip repList [0 ..])
+    idToRep = Map.fromList (zip [0 ..] repList)
     alphaList = [minBound .. maxBound] :: [i]
 
     getStateId :: [i] -> Maybe StateID
     getStateId s = List.find (equivalentRows ot s) repList >>= flip Map.lookup repToId
 
     repAt :: StateID -> Maybe [i]
-    repAt sid
-        | sid >= 0 && sid < numStates = Just (repList !! sid)
-        | otherwise = Nothing
+    repAt sid = Map.lookup sid idToRep
 
     buildDeltaEntry :: (StateID, i) -> Maybe ((StateID, i), StateID)
     buildDeltaEntry (sid, i) = do
@@ -217,10 +298,15 @@
     buildLambdaEntry :: (StateID, i) -> Maybe ((StateID, i), o)
     buildLambdaEntry (sid, i) = do
         rep <- repAt sid
-        o <- Map.lookup (rep, [i]) (mappingT ot)
-        return ((sid, i), o)
+        out <- Map.lookup (rep, [i]) (mappingT ot)
+        return ((sid, i), headLH out)
 
 -- | The 'makeConsistent' function makes the observation table consistent by adding missing prefixes.
+
+{-@ makeConsistent :: (FiniteOrd i, SUL sul m) =>
+      ObservationTable i o ->
+      ({v:[i] | len v = 1}, {v:[i] | len v >= 1}) ->
+      ExperimentT (sul i o) m (ObservationTable i o) @-}
 makeConsistent ::
     forall i o sul m.
     (FiniteOrd i, SUL sul m) =>
@@ -228,33 +314,25 @@
     ([i], [i]) ->
     ExperimentT (sul i o) m (ObservationTable i o)
 makeConsistent ot ([], []) = return ot
-makeConsistent ot (column, symbol) = do
+makeConsistent ot (symbol, column) = do
     sul <- ask
     let
         query = symbol ++ column
-        -- prefices = [take n query | n <- [1 .. length query]]
-
-        -- only the query itself must be inserted.
-        -- the suffixes are already members.
         em = suffixSetE ot
         em' = query `Set.insert` em
-
         sm = prefixSetS ot
         sm_I = prefixSetSI ot
-
         tm = mappingT ot
-
-        missing = (sm `Set.union` sm_I) `Set.cartesianProduct` em'
-        missing' = map (uncurry (++)) $ Set.toList missing
-
-    outs <- lift $ forM missing' (walk sul)
-
-    let
-        outs' = map (last . snd) outs
-        tm' = foldr (\((a, b), o) -> Map.insert (a, b) o) tm (zip (Set.toList missing) outs')
+        missing = (sm `Set.union` sm_I) `Set.cartesianProduct` Set.singleton query
+    tm' <- lift $ updateMap tm missing sul
     return (ObservationTable{prefixSetS = sm, suffixSetE = em', mappingT = tm', prefixSetSI = sm_I})
 
 -- | The 'makeClosed' function makes the observation table closed by adding missing suffixes.
+
+{-@ makeClosed :: (FiniteOrd i, SUL sul m) =>
+      ObservationTable i o ->
+      {v:[i] | len v > 0} ->
+      ExperimentT (sul i o) m (ObservationTable i o) @-}
 makeClosed ::
     forall sul i o m.
     (FiniteOrd i, SUL sul m) =>
@@ -264,37 +342,42 @@
 makeClosed ot [] = return ot
 makeClosed ot inc = do
     sul <- ask
-    let
-        alph = Set.toList $ inputs sul
+    let alph = inputs sul
         sm = prefixSetS ot
         em = suffixSetE ot
         tm = mappingT ot
         sm' = inc `Set.insert` sm
-        sm_I' = Set.fromList [w ++ [a] | w <- Set.toList sm', a <- alph]
-    outs <- lift $ forM (Set.toList em) (walk sul)
-    let mappings = [((inc ++ [s], e), last (snd o)) | s <- alph, (e, o) <- zip (Set.toList em) outs]
-        tm' = List.foldr (uncurry Map.insert) tm mappings
+        sm_I' = Set.map (\(w, a) -> w ++ [a]) (sm' `Set.cartesianProduct` alph)
+        newPrefixes = Set.map (\a -> inc ++ [a]) alph
+        missing = newPrefixes `Set.cartesianProduct` em
+    tm' <- lift $ updateMap tm missing sul
     return (ObservationTable{prefixSetS = sm', suffixSetE = em, mappingT = tm', prefixSetSI = sm_I'})
 
 instance Learner LMstar MealyAutomaton StateID where
     initialize (LMstar _) = do
-        LMstar <$> initializeOT
+        LMstar . Init <$> initializeOT
     initialize (LMplus _) = do
-        LMplus <$> initializeOT
+        LMplus . Init <$> initializeOT
 
-    refine (LMstar ot) cex = do
+    refine (LMstar (Init ot)) cex = do
         ot' <- otRefineAngluin ot cex
-        return (LMstar ot')
-    refine (LMplus ot) cex = do
+        return (LMstar (Init ot'))
+    refine (LMplus (Init ot)) cex = do
         ot' <- otRefinePlus ot cex
-        return (LMplus ot')
+        return (LMplus (Init ot'))
+    refine (LMstar Uninit) _ = initialize (LMstar Uninit)
+    refine (LMplus Uninit) _ = initialize (LMplus Uninit)
 
-    learn (LMstar ot) = lmstar (LMstar ot)
-    learn (LMplus ot) = lmstar (LMplus ot)
+    learn = lmstar
 
 {- | The 'otRefinePlus' function refines the observation table based on a counterexample, according to the LM+ algorithm,
 which is an improvement over Angluin's algorithm.
 -}
+
+{-@ otRefinePlus :: (FiniteOrd i, SUL sul m) =>
+      ObservationTable i o ->
+      [i] ->
+      ExperimentT (sul i o) m (ObservationTable i o) @-}
 otRefinePlus ::
     forall sul i o m.
     (FiniteOrd i, SUL sul m) =>
@@ -314,26 +397,48 @@
         suffixes = List.tails cex
         pairs = List.reverse $ List.zip prefixes suffixes
         wrapped = List.find (\x -> Set.member (fst x) sm || Set.member (fst x) sm_I) pairs
-        (_, suffix) = Maybe.fromMaybe (error "failed to update observation table") wrapped
-        -- the suffix is the distinguishing suffix. insert all suffixes expect from the empty one
-        newSuffixes = em `Set.difference` Set.fromList (init $ List.tails suffix)
-        em' = List.foldr Set.insert em newSuffixes
-        missing = (sm `Set.union` sm_I) `Set.cartesianProduct` newSuffixes
-    tm' <- lift $ updateMap tm missing sul
-    return (ObservationTable{prefixSetS = sm, suffixSetE = em', mappingT = tm', prefixSetSI = sm_I})
+    case wrapped of
+        Nothing -> return ot
+        -- TODO: suffix triggers liquid haskell false
+        Just (_, suffix) -> do
+            let
+                -- the suffix is the distinguishing suffix. insert all non-empty tails not already in E
+                newSuffixes = Set.fromList (init $ List.tails suffix) `Set.difference` em
+                em' = List.foldr Set.insert em newSuffixes
+                missing = (sm `Set.union` sm_I) `Set.cartesianProduct` newSuffixes
+            tm' <- lift $ updateMap tm missing sul
+            return (ObservationTable{prefixSetS = sm, suffixSetE = em', mappingT = tm', prefixSetSI = sm_I})
 
+{-@ insertStep
+      :: (Ord i, SUL sul m, Monad m)
+      => sul i o
+      -> Map.Map ([i],[i]) {v:[o] | len v > 0}
+      -> ([i], {b:[i] | len b > 0})
+      -> m (Map.Map ([i],[i]) {v:[o] | len v > 0}) @-}
+insertStep ::
+    (Ord i, SUL sul m, Monad m) =>
+    sul i o ->
+    Map.Map ([i], [i]) [o] ->
+    ([i], [i]) ->
+    m (Map.Map ([i], [i]) [o])
+insertStep thesul acc (a, b) = do
+    (_, outs) <- walk thesul (a ++ b)
+    -- the table is prefix closed, so no need to store
+    -- the whole length of outs, just the output that corresponds
+    -- to the suffix
+    pure (Map.insert (a, b) (dropLH outs (length a)) acc)
+
+{-@ updateMap
+      :: (Ord i, SUL sul m, Monad m)
+      => Map.Map ([i],[i]) {v:[o] | len v > 0}
+      -> Set.Set ([i], {v:[i] | len v > 0})
+      -> sul i o
+      -> m (Map.Map ([i],[i]) {v:[o] | len v > 0}) @-}
 updateMap ::
     (Ord i, SUL sul m, Monad m) =>
-    Map.Map ([i], [i]) o ->
+    Map.Map ([i], [i]) [o] ->
     Set.Set ([i], [i]) ->
     sul i o ->
-    m (Map.Map ([i], [i]) o)
+    m (Map.Map ([i], [i]) [o])
 updateMap themap thestuff thesul =
-    foldM
-        ( \acc (a, b) -> do
-            (_, outs) <- walk thesul (a ++ b)
-            let o = last outs
-            pure (Map.insert (a, b) o acc)
-        )
-        themap
-        thestuff
+    foldM (insertStep thesul) themap thestuff