diff --git a/cabal.project b/cabal.project
index 43367b3182..79d8a4d894 100644
--- a/cabal.project
+++ b/cabal.project
@@ -31,5 +31,4 @@ packages:
     deps/dwarf
     deps/argo/argo
     deps/argo/tasty-script-exitcode
-    deps/argo/python
     deps/cryptol/cryptol-remote-api
diff --git a/deps/argo b/deps/argo
index f05207fecf..1040dc26d1 160000
--- a/deps/argo
+++ b/deps/argo
@@ -1 +1 @@
-Subproject commit f05207fecfd455dc3fe18fb52de661bae9b207bc
+Subproject commit 1040dc26d142f13ff8ed6617ff5212f476b78c45
diff --git a/deps/cryptol b/deps/cryptol
index 8f914a7b88..40626a3061 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit 8f914a7b8815718d4e510966199045e0bec4d099
+Subproject commit 40626a3061c4667dc332344b5a64d5292bb789d6
diff --git a/saw-remote-api/saw-remote-api/Main.hs b/saw-remote-api/saw-remote-api/Main.hs
index c3a8adc77f..4a6958d6a5 100644
--- a/saw-remote-api/saw-remote-api/Main.hs
+++ b/saw-remote-api/saw-remote-api/Main.hs
@@ -1,25 +1,43 @@
 {-# LANGUAGE OverloadedStrings #-}
 module Main (main) where
 
-import Argo
-import Argo.DefaultMain
+import qualified Argo
+import qualified Argo.DefaultMain as Argo (defaultMain)
 import qualified Argo.Doc as Doc
 
-import SAWServer
+import SAWServer ( SAWState, initialState )
 import SAWServer.CryptolSetup
+    ( cryptolLoadModuleDescr,
+      cryptolLoadModule,
+      cryptolLoadFileDescr,
+      cryptolLoadFile )
 --import SAWServer.JVMCrucibleSetup
 --import SAWServer.JVMVerify
 import SAWServer.LLVMCrucibleSetup
+    ( llvmLoadModuleDescr, llvmLoadModule )
 import SAWServer.LLVMVerify
+    ( llvmVerifyDescr,
+      llvmVerify,
+      llvmAssumeDescr,
+      llvmAssume,
+      llvmVerifyX86Descr,
+      llvmVerifyX86 )
 import SAWServer.ProofScript
-import SAWServer.SaveTerm
-import SAWServer.SetOption
+    ( makeSimpsetDescr, makeSimpset, proveDescr, prove )
+import SAWServer.SaveTerm ( saveTermDescr, saveTerm )
+import SAWServer.SetOption ( setOptionDescr, setOption )
 
 
 main :: IO ()
-main =
-  do theApp <- mkDefaultApp "SAW RPC Server" serverDocs initialState sawMethods
-     defaultMain description theApp
+main = do
+  theApp <- Argo.mkApp
+               "SAW RPC Server"
+               serverDocs
+               (Argo.defaultAppOpts
+               Argo.MutableState)
+               initialState
+               sawMethods
+  Argo.defaultMain description theApp
 
 serverDocs :: [Doc.Block]
 serverDocs =
@@ -32,65 +50,55 @@ description :: String
 description =
   "An RPC server for SAW."
 
-sawMethods :: [AppMethod SAWState]
+sawMethods :: [Argo.AppMethod SAWState]
 sawMethods =
   -- Cryptol
-  [ method
+  [ Argo.command
      "SAW/Cryptol/load module"
-     Command
      cryptolLoadModuleDescr
      cryptolLoadModule
-  , method
+  , Argo.command
      "SAW/Cryptol/load file"
-     Command
      cryptolLoadFileDescr
      cryptolLoadFile
-  , method
+  , Argo.command
      "SAW/Cryptol/save term"
-     Command
      saveTermDescr
      saveTerm
   -- JVM
   {-
-  , method "SAW/JVM/load class" Command (Doc.Paragraph [Doc.Text "TODO"]) jvmLoadClass
-  , method "SAW/JVM/verify"     Command (Doc.Paragraph [Doc.Text "TODO"]) jvmVerify
-  , method "SAW/JVM/assume"     Command (Doc.Paragraph [Doc.Text "TODO"]) jvmAssume
+  , Argo.command "SAW/JVM/load class" (Doc.Paragraph [Doc.Text "TODO"]) jvmLoadClass
+  , Argo.command "SAW/JVM/verify"     (Doc.Paragraph [Doc.Text "TODO"]) jvmVerify
+  , Argo.command "SAW/JVM/assume"     (Doc.Paragraph [Doc.Text "TODO"]) jvmAssume
   -}
   -- LLVM
-  , method
+  , Argo.command
      "SAW/LLVM/load module"
-     Command
      llvmLoadModuleDescr
      llvmLoadModule
-  , method
+  , Argo.command
      "SAW/LLVM/verify"
-     Command
      llvmVerifyDescr
      llvmVerify
-  , method
+  , Argo.command
      "SAW/LLVM/verify x86"
-     Command
      llvmVerifyX86Descr
      llvmVerifyX86
-  , method
+  , Argo.command
      "SAW/LLVM/assume"
-     Command
      llvmAssumeDescr
      llvmAssume
   -- General
-  , method
+  , Argo.command
      "SAW/make simpset"
-     Command
      makeSimpsetDescr
      makeSimpset
-  , method
+  , Argo.command
      "SAW/prove"
-     Command
      proveDescr
      prove
-  , method
+  , Argo.command
      "SAW/set option"
-     Command
      setOptionDescr
      setOption
   ]
diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs
index decadf63eb..672e2fe50d 100644
--- a/saw-remote-api/src/SAWServer.hs
+++ b/saw-remote-api/src/SAWServer.hs
@@ -7,19 +7,20 @@
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
 module SAWServer
   ( module SAWServer
   ) where
 
 import Prelude hiding (mod)
-import Control.Lens
+import Control.Lens ( Lens', view, lens, over )
 import Data.Aeson (FromJSON(..), ToJSON(..), withText)
 import Data.ByteString (ByteString)
 import Data.Kind (Type)
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as M
-import Data.Parameterized.Pair
-import Data.Parameterized.Some
+import Data.Parameterized.Pair ( Pair(..) )
+import Data.Parameterized.Some ( Some(..) )
 import Data.Text (Text)
 import qualified Data.Text as T
 import qualified Crypto.Hash as Hash
@@ -58,9 +59,17 @@ import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm)
 import Verifier.SAW.Rewriter (Simpset)
 import qualified Cryptol.Utils.Ident as Cryptol
 
-import Argo
+import qualified Argo
 import qualified CryptolServer (validateServerState, ServerState(..))
 import SAWServer.Exceptions
+    ( serverValNotFound,
+      notAnLLVMModule,
+      notAnLLVMSetup,
+      notAnLLVMMethodSpecIR,
+      notASimpset,
+      notATerm,
+      notAJVMClass,
+      notAJVMMethodSpecIR )
 
 type SAWCont = (SAWEnv, SAWTask)
 
@@ -144,19 +153,19 @@ trackedFiles :: Lens' SAWState (Map FilePath (Hash.Digest Hash.SHA256))
 trackedFiles = lens _trackedFiles (\v tf -> v { _trackedFiles = tf })
 
 
-pushTask :: SAWTask -> Method SAWState ()
-pushTask t = modifyState mod
+pushTask :: SAWTask -> Argo.Command SAWState ()
+pushTask t = Argo.modifyState mod
   where mod (SAWState env bic stack ro rw tf) =
           SAWState env bic ((t, env) : stack) ro rw tf
 
-dropTask :: Method SAWState ()
-dropTask = modifyState mod
+dropTask :: Argo.Command SAWState ()
+dropTask = Argo.modifyState mod
   where mod (SAWState _ _ [] _ _ _) = error "Internal error - stack underflow"
         mod (SAWState _ sc ((_t, env):stack) ro rw tf) =
           SAWState env sc stack ro rw tf
 
-getHandleAlloc :: Method SAWState Crucible.HandleAllocator
-getHandleAlloc = roHandleAlloc . view sawTopLevelRO <$> getState
+getHandleAlloc :: Argo.Command SAWState Crucible.HandleAllocator
+getHandleAlloc = roHandleAlloc . view sawTopLevelRO <$> Argo.getState
 
 initialState :: (FilePath -> IO ByteString) -> IO SAWState
 initialState readFileFn =
@@ -326,77 +335,77 @@ instance KnownCrucibleSetupType a => IsServerVal (LLVMCrucibleSetupM a) where
 instance IsServerVal (Some CMS.LLVMModule) where
   toServerVal = VLLVMModule
 
-setServerVal :: IsServerVal val => ServerName -> val -> Method SAWState ()
+setServerVal :: IsServerVal val => ServerName -> val -> Argo.Command SAWState ()
 setServerVal name val =
-  do debugLog $ "Saving " <> (T.pack (show name))
-     modifyState $
+  do Argo.debugLog $ "Saving " <> (T.pack (show name))
+     Argo.modifyState $
        over sawEnv $
        \(SAWEnv env) ->
          SAWEnv (M.insert name (toServerVal val) env)
-     debugLog $ "Saved " <> (T.pack (show name))
-     st <- getState
-     debugLog $ "State is " <> T.pack (show st)
+     Argo.debugLog $ "Saved " <> (T.pack (show name))
+     st <- Argo.getState @SAWState
+     Argo.debugLog $ "State is " <> T.pack (show st)
 
 
-getServerVal :: ServerName -> Method SAWState ServerVal
+getServerVal :: ServerName -> Argo.Command SAWState ServerVal
 getServerVal n =
-  do SAWEnv serverEnv <- view sawEnv <$> getState
-     st <- getState
-     debugLog $ "Looking up " <> T.pack (show n) <> " in " <> T.pack (show st)
+  do SAWEnv serverEnv <- view sawEnv <$> Argo.getState
+     st <- Argo.getState @SAWState
+     Argo.debugLog $ "Looking up " <> T.pack (show n) <> " in " <> T.pack (show st)
      case M.lookup n serverEnv of
-       Nothing -> raise (serverValNotFound n)
+       Nothing -> Argo.raise (serverValNotFound n)
        Just val -> return val
 
-bindCryptolVar :: Text -> TypedTerm -> Method SAWState ()
+bindCryptolVar :: Text -> TypedTerm -> Argo.Command SAWState ()
 bindCryptolVar x t =
-  do modifyState $ over sawTopLevelRW $ \rw ->
+  do Argo.modifyState $ over sawTopLevelRW $ \rw ->
        rw { rwCryptol = bindTypedTerm (Cryptol.mkIdent x, t) (rwCryptol rw) }
 
-getJVMClass :: ServerName -> Method SAWState JSS.Class
+getJVMClass :: ServerName -> Argo.Command SAWState JSS.Class
 getJVMClass n =
   do v <- getServerVal n
      case v of
        VJVMClass c -> return c
-       _other -> raise (notAJVMClass n)
+       _other -> Argo.raise (notAJVMClass n)
 
-getJVMMethodSpecIR :: ServerName -> Method SAWState (CMS.CrucibleMethodSpecIR CJ.JVM)
+getJVMMethodSpecIR :: ServerName -> Argo.Command SAWState (CMS.CrucibleMethodSpecIR CJ.JVM)
 getJVMMethodSpecIR n =
   do v <- getServerVal n
      case v of
        VJVMMethodSpecIR ir -> return ir
-       _other -> raise (notAJVMMethodSpecIR n)
+       _other -> Argo.raise (notAJVMMethodSpecIR n)
 
-getLLVMModule :: ServerName -> Method SAWState (Some CMS.LLVMModule)
+getLLVMModule :: ServerName -> Argo.Command SAWState (Some CMS.LLVMModule)
 getLLVMModule n =
   do v <- getServerVal n
      case v of
        VLLVMModule m -> return m
-       _other -> raise (notAnLLVMModule n)
+       _other -> Argo.raise (notAnLLVMModule n)
 
-getLLVMSetup :: ServerName -> Method SAWState (Pair CrucibleSetupTypeRepr LLVMCrucibleSetupM)
+getLLVMSetup :: ServerName -> Argo.Command SAWState (Pair CrucibleSetupTypeRepr LLVMCrucibleSetupM)
 getLLVMSetup n =
   do v <- getServerVal n
      case v of
        VLLVMCrucibleSetup setup -> return setup
-       _other -> raise (notAnLLVMSetup n)
+       _other -> Argo.raise (notAnLLVMSetup n)
 
-getLLVMMethodSpecIR :: ServerName -> Method SAWState (CMS.SomeLLVM CMS.CrucibleMethodSpecIR)
+getLLVMMethodSpecIR :: ServerName -> Argo.Command SAWState (CMS.SomeLLVM CMS.CrucibleMethodSpecIR)
 getLLVMMethodSpecIR n =
   do v <- getServerVal n
      case v of
        VLLVMMethodSpecIR ir -> return ir
-       _other -> raise (notAnLLVMMethodSpecIR n)
+       _other -> Argo.raise (notAnLLVMMethodSpecIR n)
 
-getSimpset :: ServerName -> Method SAWState Simpset
+getSimpset :: ServerName -> Argo.Command SAWState Simpset
 getSimpset n =
   do v <- getServerVal n
      case v of
        VSimpset ss -> return ss
-       _other -> raise (notASimpset n)
+       _other -> Argo.raise (notASimpset n)
 
-getTerm :: ServerName -> Method SAWState TypedTerm
+getTerm :: ServerName -> Argo.Command SAWState TypedTerm
 getTerm n =
   do v <- getServerVal n
      case v of
        VTerm t -> return t
-       _other -> raise (notATerm n)
+       _other -> Argo.raise (notATerm n)
diff --git a/saw-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs
index 6da82d66ee..5af4d95c19 100644
--- a/saw-remote-api/src/SAWServer/CryptolExpression.hs
+++ b/saw-remote-api/src/SAWServer/CryptolExpression.hs
@@ -3,23 +3,16 @@
 {-# LANGUAGE PartialTypeSignatures #-}
 {-# LANGUAGE TupleSections #-}
 module SAWServer.CryptolExpression
- (getCryptolExpr
+ ( getCryptolExpr
  , getTypedTerm
  , getTypedTermOfCExp
  ) where
 
-import Control.Lens hiding (re)
-import Control.Monad.IO.Class
+import Control.Lens ( view )
+import Control.Monad.IO.Class ( MonadIO(liftIO) )
 import qualified Data.ByteString as B
-import qualified Data.HashMap.Strict as HM
 import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
-import Data.List.NonEmpty (NonEmpty(..))
-import qualified Data.ByteString.Base64 as Base64
-import Data.Text (Text)
-import qualified Data.Text as T
-import Data.Text.Encoding (encodeUtf8)
-import Data.Traversable (for)
 
 import Cryptol.Eval (EvalOpts(..))
 import Cryptol.ModuleSystem (ModuleRes, ModuleInput(..))
@@ -28,34 +21,35 @@ import Cryptol.ModuleSystem.Env (ModuleEnv, meSolverConfig)
 import Cryptol.ModuleSystem.Interface (noIfaceParams)
 import Cryptol.ModuleSystem.Monad (ModuleM, interactive, runModuleM, setNameSeeds, setSupply, typeCheckWarnings, typeCheckingFailed)
 import qualified Cryptol.ModuleSystem.Renamer as MR
-import Cryptol.Parser.AST
-import qualified Cryptol.Parser as CP
+import Cryptol.Parser.AST ( Expr, PName )
 import Cryptol.Parser.Position (emptyRange, getLoc)
 import Cryptol.TypeCheck (tcExpr)
 import Cryptol.TypeCheck.Monad (InferOutput(..), inpVars, inpTSyns)
 import Cryptol.TypeCheck.Solver.SMT (withSolver)
 import Cryptol.Utils.Ident (interactiveName)
 import Cryptol.Utils.Logger (quietLogger)
-import Cryptol.Utils.PP
-import Cryptol.Utils.RecordMap (recordFromFields)
+import Cryptol.Utils.PP ( defaultPPOpts, pp )
 import SAWScript.Value (biSharedContext, TopLevelRW(..))
 import Verifier.SAW.CryptolEnv
+    ( getAllIfaceDecls,
+      getNamingEnv,
+      translateExpr,
+      CryptolEnv(eExtraTypes, eExtraTSyns, eModuleEnv) )
 import Verifier.SAW.SharedTerm (SharedContext)
 import Verifier.SAW.TypedTerm(TypedTerm(..))
 
-import Argo
-import CryptolServer.Data.Expression (Expression(..), TypeArguments(..), LetBinding(..), Encoding(..), bytesToInt)
-import CryptolServer.Data.Type (JSONPType(..))
+import qualified Argo
+import CryptolServer.Data.Expression (Expression, getCryptolExpr)
+import CryptolServer.Exceptions (cryptolError)
 import SAWServer
-import CryptolServer.Exceptions (cryptolError, cryptolParseErr, invalidHex, invalidBase64)
 
-getTypedTerm :: Expression -> Method SAWState TypedTerm
+getTypedTerm :: Expression -> Argo.Command SAWState TypedTerm
 getTypedTerm inputExpr =
-  do cenv <- rwCryptol . view sawTopLevelRW <$> getState
-     fileReader <- getFileReader
+  do cenv <- rwCryptol . view sawTopLevelRW <$> Argo.getState
+     fileReader <- Argo.getFileReader
      expr <- getCryptolExpr inputExpr
-     sc <- biSharedContext . view sawBIC <$> getState
-     (t, _) <- moduleCmdResult =<< (liftIO $ getTypedTermOfCExp fileReader sc cenv expr)
+     sc <- biSharedContext . view sawBIC <$> Argo.getState
+     (t, _) <- moduleCmdResult =<< liftIO (getTypedTermOfCExp fileReader sc cenv expr)
      return t
 
 getTypedTermOfCExp ::
@@ -92,12 +86,12 @@ getTypedTermOfCExp fileReader sc cenv expr =
             return (Right (TypedTerm schema trm, modEnv'), ws)
        (Left err, ws) -> return (Left err, ws)
 
-moduleCmdResult :: ModuleRes a -> Method SAWState (a, ModuleEnv)
+moduleCmdResult :: ModuleRes a -> Argo.Command SAWState (a, ModuleEnv)
 moduleCmdResult (result, warnings) =
   do mapM_ (liftIO . print . pp) warnings
      case result of
        Right (a, me) -> return (a, me)
-       Left err      -> raise $ cryptolError err warnings
+       Left err      -> Argo.raise $ cryptolError err warnings
 
 defaultEvalOpts :: EvalOpts
 defaultEvalOpts = EvalOpts quietLogger defaultPPOpts
@@ -114,109 +108,3 @@ runInferOutput out =
     InferFailed nm warns errs ->
       do typeCheckWarnings nm warns
          typeCheckingFailed nm errs
-
-
-
--- FIXME REFACTOR/REMOVE `decode` -- it exists in
--- `cryptol-remote-api` but with less polymorphic type.
-decode :: Encoding -> Text -> Argo.Method s Integer
-decode Base64 txt =
-  let bytes = encodeUtf8 txt
-  in
-    case Base64.decode bytes of
-      Left err ->
-        Argo.raise (invalidBase64 bytes err)
-      Right decoded -> return $ bytesToInt decoded
-decode Hex txt =
-  squish <$> traverse hexDigit (T.unpack txt)
-  where
-    squish = foldl (\acc i -> (acc * 16) + i) 0
-
--- FIXME REFACTOR/REMOVE `hexDigit` -- it exists in
--- `cryptol-remote-api` but with less polymorphic type.
-hexDigit :: Num a => Char -> Argo.Method s a
-hexDigit '0' = pure 0
-hexDigit '1' = pure 1
-hexDigit '2' = pure 2
-hexDigit '3' = pure 3
-hexDigit '4' = pure 4
-hexDigit '5' = pure 5
-hexDigit '6' = pure 6
-hexDigit '7' = pure 7
-hexDigit '8' = pure 8
-hexDigit '9' = pure 9
-hexDigit 'a' = pure 10
-hexDigit 'A' = pure 10
-hexDigit 'b' = pure 11
-hexDigit 'B' = pure 11
-hexDigit 'c' = pure 12
-hexDigit 'C' = pure 12
-hexDigit 'd' = pure 13
-hexDigit 'D' = pure 13
-hexDigit 'e' = pure 14
-hexDigit 'E' = pure 14
-hexDigit 'f' = pure 15
-hexDigit 'F' = pure 15
-hexDigit c   = Argo.raise (invalidHex c)
-
--- FIXME REFACTOR/REMOVE `getCryptolExpr` -- it exists in
--- `cryptol-remote-api` (as `getExpr`) but with less polymorphic type.
-getCryptolExpr :: Expression -> Argo.Method s (Expr PName)
-getCryptolExpr Unit =
-  return $
-    ETyped
-      (ETuple [])
-      (TTuple [])
-getCryptolExpr (Bit b) =
-  return $
-    ETyped
-      (EVar (UnQual (mkIdent $ if b then "True" else "False")))
-      TBit
-getCryptolExpr (Integer i) =
-  return $
-    ETyped
-      (ELit (ECNum i (DecLit (T.pack (show i)))))
-      (TUser (UnQual (mkIdent "Integer")) [])
-getCryptolExpr (IntegerModulo i n) =
-  return $
-    ETyped
-      (ELit (ECNum i (DecLit (T.pack (show i)))))
-      (TUser (UnQual (mkIdent "Z")) [TNum n])
-getCryptolExpr (Num enc txt w) =
-  do d <- decode enc txt
-     return $ ETyped
-       (ELit (ECNum d (DecLit txt)))
-       (TSeq (TNum w) TBit)
-getCryptolExpr (Record fields) =
-  fmap (ERecord . recordFromFields) $ for (HM.toList fields) $
-  \(recName, spec) ->
-    (mkIdent recName,) . (emptyRange,) <$> getCryptolExpr spec
-getCryptolExpr (Sequence elts) =
-  EList <$> traverse getCryptolExpr elts
-getCryptolExpr (Tuple projs) =
-  ETuple <$> traverse getCryptolExpr projs
-getCryptolExpr (Concrete syntax) =
-  case CP.parseExpr syntax of
-    Left err ->
-      Argo.raise (cryptolParseErr syntax err)
-    Right e -> pure e
-getCryptolExpr (Let binds body) =
-  EWhere <$> getCryptolExpr body <*> traverse mkBind binds
-  where
-    mkBind (LetBinding x rhs) =
-      DBind .
-      (\bindBody ->
-         Bind (fakeLoc (UnQual (mkIdent x))) [] bindBody Nothing False Nothing [] True Nothing) .
-      fakeLoc .
-      DExpr <$>
-        getCryptolExpr rhs
-
-    fakeLoc = Located emptyRange
-getCryptolExpr (Application fun (arg :| [])) =
-  EApp <$> getCryptolExpr fun <*> getCryptolExpr arg
-getCryptolExpr (Application fun (arg1 :| (arg : args))) =
-  getCryptolExpr (Application (Application fun (arg1 :| [])) (arg :| args))
-getCryptolExpr (TypeApplication gen (TypeArguments args)) =
-  EAppT <$> getCryptolExpr gen <*> pure (map inst (Map.toList args))
-  where
-    inst (n, t) = NamedInst (Named (Located emptyRange n) (unJSONPType t))
diff --git a/saw-remote-api/src/SAWServer/CryptolSetup.hs b/saw-remote-api/src/SAWServer/CryptolSetup.hs
index 2c769689e1..09c65a161e 100644
--- a/saw-remote-api/src/SAWServer/CryptolSetup.hs
+++ b/saw-remote-api/src/SAWServer/CryptolSetup.hs
@@ -10,8 +10,8 @@ module SAWServer.CryptolSetup
   ) where
 
 import Control.Exception (SomeException, try)
-import Control.Monad.IO.Class
-import Control.Lens
+import Control.Monad.IO.Class ( MonadIO(liftIO) )
+import Control.Lens ( view, over )
 import Data.Aeson (FromJSON(..), withObject, (.:))
 import qualified Data.Text as T
 
@@ -20,32 +20,32 @@ import Cryptol.Utils.Ident (textToModName)
 import SAWScript.Value (biSharedContext, rwCryptol)
 import qualified Verifier.SAW.CryptolEnv as CEnv
 
-import Argo
+import qualified Argo
 import qualified Argo.Doc as Doc
-import SAWServer
-import SAWServer.Exceptions
-import SAWServer.OK
+import SAWServer ( SAWState, sawBIC, sawTopLevelRW )
+import SAWServer.Exceptions ( cryptolError )
+import SAWServer.OK ( OK, ok )
 
 cryptolLoadModuleDescr :: Doc.Block
 cryptolLoadModuleDescr =
   Doc.Paragraph [Doc.Text "Load the specified Cryptol module."]
 
-cryptolLoadModule :: CryptolLoadModuleParams -> Method SAWState OK
+cryptolLoadModule :: CryptolLoadModuleParams -> Argo.Command SAWState OK
 cryptolLoadModule (CryptolLoadModuleParams modName) =
-  do sc <- biSharedContext . view sawBIC <$> getState
-     cenv <- rwCryptol . view sawTopLevelRW <$> getState
+  do sc <- biSharedContext . view sawBIC <$> Argo.getState
+     cenv <- rwCryptol . view sawTopLevelRW <$> Argo.getState
      let qual = Nothing -- TODO add field to params
      let importSpec = Nothing -- TODO add field to params
-     fileReader <- getFileReader
+     fileReader <- Argo.getFileReader
      let ?fileReader = fileReader
      cenv' <- liftIO $ try $ CEnv.importModule sc cenv (Right modName) qual CEnv.PublicAndPrivate importSpec
      case cenv' of
-       Left (ex :: SomeException) -> raise $ cryptolError (show ex)
+       Left (ex :: SomeException) -> Argo.raise $ cryptolError (show ex)
        Right cenv'' ->
-         do modifyState $ over sawTopLevelRW $ \rw -> rw { rwCryptol = cenv'' }
+         do Argo.modifyState $ over sawTopLevelRW $ \rw -> rw { rwCryptol = cenv'' }
             ok
 
-data CryptolLoadModuleParams =
+newtype CryptolLoadModuleParams =
   CryptolLoadModuleParams P.ModName
 
 instance FromJSON CryptolLoadModuleParams where
@@ -65,22 +65,22 @@ cryptolLoadFileDescr =
   Doc.Paragraph [Doc.Text "Load the given file as a Cryptol module."]
 
 
-cryptolLoadFile :: CryptolLoadFileParams -> Method SAWState OK
+cryptolLoadFile :: CryptolLoadFileParams -> Argo.Command SAWState OK
 cryptolLoadFile (CryptolLoadFileParams fileName) =
-  do sc <- biSharedContext . view sawBIC <$> getState
-     cenv <- rwCryptol . view sawTopLevelRW <$> getState
+  do sc <- biSharedContext . view sawBIC <$> Argo.getState
+     cenv <- rwCryptol . view sawTopLevelRW <$> Argo.getState
      let qual = Nothing -- TODO add field to params
      let importSpec = Nothing -- TODO add field to params
-     fileReader <- getFileReader
+     fileReader <- Argo.getFileReader
      let ?fileReader = fileReader
      cenv' <- liftIO $ try $ CEnv.importModule sc cenv (Left fileName) qual CEnv.PublicAndPrivate importSpec
      case cenv' of
-       Left (ex :: SomeException) -> raise $ cryptolError (show ex)
+       Left (ex :: SomeException) -> Argo.raise $ cryptolError (show ex)
        Right cenv'' ->
-         do modifyState $ over sawTopLevelRW $ \rw -> rw { rwCryptol = cenv'' }
+         do Argo.modifyState $ over sawTopLevelRW $ \rw -> rw { rwCryptol = cenv'' }
             ok
 
-data CryptolLoadFileParams =
+newtype CryptolLoadFileParams =
   CryptolLoadFileParams FilePath
 
 instance FromJSON CryptolLoadFileParams where
diff --git a/saw-remote-api/src/SAWServer/Exceptions.hs b/saw-remote-api/src/SAWServer/Exceptions.hs
index 60567ceb08..d02a1016aa 100644
--- a/saw-remote-api/src/SAWServer/Exceptions.hs
+++ b/saw-remote-api/src/SAWServer/Exceptions.hs
@@ -23,11 +23,11 @@ module SAWServer.Exceptions (
   , verificationException
   ) where
 
-import Control.Exception
-import Data.Aeson as JSON
+import Control.Exception ( Exception(displayException) )
+import Data.Aeson as JSON ( object, KeyValue((.=)), ToJSON )
 import qualified Data.Text as T
 
-import Argo
+import Argo ( makeJSONRPCException, JSONRPCException )
 
 --------------------------------------------------------------------------------
 -- NOTE: IF YOU MODIFY EXCEPTION CODES OR ADD NEW ONES, THESE CHANGES MUST BE
diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
index f190ccc725..16e3121c66 100644
--- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs
@@ -13,15 +13,20 @@ module SAWServer.JVMCrucibleSetup
   , compileJVMContract
   ) where
 
-import Control.Lens
-import Control.Monad.IO.Class
+import Control.Lens ( view )
+import Control.Monad.IO.Class ( MonadIO(liftIO) )
 import Control.Monad.State
+    ( evalStateT,
+      MonadState(get, put),
+      MonadTrans(lift),
+      modify' )
 import Data.Aeson (FromJSON(..), withObject, (.:))
 import Data.ByteString (ByteString)
-import Data.Foldable
+import Data.Foldable ( traverse_ )
+import Data.Functor (($>))
 import Data.Map (Map)
 import qualified Data.Map as Map
-import Data.Maybe
+import Data.Maybe ( maybeToList )
 import qualified Data.Text as T
 
 import qualified Cryptol.Parser.AST as P
@@ -29,29 +34,50 @@ import Cryptol.Utils.Ident (mkIdent)
 import qualified Lang.Crucible.JVM as CJ
 import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..))
 import SAWScript.Crucible.JVM.Builtins
-import SAWScript.Crucible.JVM.BuiltinsJVM
+    ( jvm_alloc_array,
+      jvm_alloc_object,
+      jvm_execute_func,
+      jvm_fresh_var,
+      jvm_postcond,
+      jvm_precond,
+      jvm_return )
+import SAWScript.Crucible.JVM.BuiltinsJVM ( loadJavaClass )
 import SAWScript.JavaExpr (JavaType(..))
 import SAWScript.Value (BuiltinContext, JVMSetupM(..), biSharedContext)
 import qualified Verifier.SAW.CryptolEnv as CEnv
 import Verifier.SAW.CryptolEnv (CryptolEnv)
 import Verifier.SAW.TypedTerm (TypedTerm)
 
-import Argo
+import qualified Argo
 import qualified Argo.Doc as Doc
 import SAWServer
+    ( ServerName(..),
+      SAWState,
+      SetupStep(..),
+      CrucibleSetupVal(CryptolExpr, NullValue, NamedValue),
+      SAWTask(JVMSetup),
+      sawTask,
+      pushTask,
+      setServerVal )
 import SAWServer.Data.Contract
+    ( PointsTo(PointsTo),
+      Allocated(Allocated),
+      ContractVar(ContractVar),
+      Contract(preVars, preConds, preAllocated, prePointsTos,
+               argumentVals, postVars, postConds, postAllocated, postPointsTos,
+               returnVal) )
 import SAWServer.Data.SetupValue ()
 import SAWServer.CryptolExpression (getTypedTermOfCExp)
-import SAWServer.Exceptions
-import SAWServer.OK
-import SAWServer.TopLevel
+import SAWServer.Exceptions ( notAtTopLevel )
+import SAWServer.OK ( OK, ok )
+import SAWServer.TopLevel ( tl )
 
-startJVMSetup :: StartJVMSetupParams -> Method SAWState OK
+startJVMSetup :: StartJVMSetupParams -> Argo.Command SAWState OK
 startJVMSetup (StartJVMSetupParams n) =
   do pushTask (JVMSetup n [])
      ok
 
-data StartJVMSetupParams
+newtype StartJVMSetupParams
   = StartJVMSetupParams ServerName
 
 instance FromJSON StartJVMSetupParams where
@@ -65,7 +91,7 @@ instance Doc.DescribedParams StartJVMSetupParams where
        Doc.Paragraph [Doc.Text "The name of the item to setup on the server."])
     ]
 
-data ServerSetupVal = Val (SetupValue CJ.JVM)
+newtype ServerSetupVal = Val (SetupValue CJ.JVM)
 
 -- TODO: this is an extra layer of indirection that could be collapsed, but is easy to implement for now.
 compileJVMContract ::
@@ -96,7 +122,7 @@ interpretJVMSetup ::
   CryptolEnv ->
   [SetupStep JavaType] ->
   JVMSetupM ()
-interpretJVMSetup fileReader bic cenv0 ss = runStateT (traverse_ go ss) (mempty, cenv0) *> pure ()
+interpretJVMSetup fileReader bic cenv0 ss = evalStateT (traverse_ go ss) (mempty, cenv0)
   where
     go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= jvm_return
     -- TODO: do we really want two names here?
@@ -185,11 +211,11 @@ instance FromJSON JVMLoadClassParams where
     withObject "params for \"SAW/JVM/load class\"" $ \o ->
     JVMLoadClassParams <$> o .: "name" <*> o .: "class"
 
-jvmLoadClass :: JVMLoadClassParams -> Method SAWState OK
+jvmLoadClass :: JVMLoadClassParams -> Argo.Command SAWState OK
 jvmLoadClass (JVMLoadClassParams serverName cname) =
-  do tasks <- view sawTask <$> getState
+  do tasks <- view sawTask <$> Argo.getState
      case tasks of
-       (_:_) -> raise $ notAtTopLevel $ map fst tasks
+       (_:_) -> Argo.raise $ notAtTopLevel $ map fst tasks
        [] ->
          do c <- tl $ loadJavaClass cname
             setServerVal serverName c
diff --git a/saw-remote-api/src/SAWServer/JVMVerify.hs b/saw-remote-api/src/SAWServer/JVMVerify.hs
index c34bc59c24..82eeb6f126 100644
--- a/saw-remote-api/src/SAWServer/JVMVerify.hs
+++ b/saw-remote-api/src/SAWServer/JVMVerify.hs
@@ -9,32 +9,45 @@ import Prelude hiding (mod)
 import Control.Lens
 
 import SAWScript.Crucible.JVM.Builtins
+    ( jvm_unsafe_assume_spec, jvm_verify )
 import SAWScript.JavaExpr (JavaType(..))
 import SAWScript.Value (rwCryptol)
 
-import Argo
+import qualified Argo
 import SAWServer
+    ( SAWState,
+      SAWTask(JVMSetup),
+      sawBIC,
+      sawTask,
+      sawTopLevelRW,
+      pushTask,
+      dropTask,
+      setServerVal,
+      getJVMClass,
+      getJVMMethodSpecIR )
 import SAWServer.CryptolExpression (getCryptolExpr)
-import SAWServer.Data.Contract
-import SAWServer.Exceptions
-import SAWServer.JVMCrucibleSetup
-import SAWServer.OK
+import SAWServer.Data.Contract ( ContractMode(..) )
+import SAWServer.Exceptions ( notAtTopLevel )
+import SAWServer.JVMCrucibleSetup ( compileJVMContract )
+import SAWServer.OK ( OK, ok )
 import SAWServer.ProofScript
-import SAWServer.TopLevel
+    ( ProofScript(ProofScript), interpretProofScript )
+import SAWServer.TopLevel ( tl )
 import SAWServer.VerifyCommon
+    ( AssumeParams(AssumeParams), VerifyParams(VerifyParams) )
 
-jvmVerifyAssume :: ContractMode -> VerifyParams JavaType -> Method SAWState OK
+jvmVerifyAssume :: ContractMode -> VerifyParams JavaType -> Argo.Command SAWState OK
 jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract script lemmaName) =
-  do tasks <- view sawTask <$> getState
+  do tasks <- view sawTask <$> Argo.getState
      case tasks of
-       (_:_) -> raise $ notAtTopLevel $ map fst tasks
+       (_:_) -> Argo.raise $ notAtTopLevel $ map fst tasks
        [] ->
          do pushTask (JVMSetup lemmaName [])
-            state <- getState
+            state <- Argo.getState
             cls <- getJVMClass className
             let bic = view sawBIC state
                 cenv = rwCryptol (view sawTopLevelRW state)
-            fileReader <- getFileReader
+            fileReader <- Argo.getFileReader
             setup <- compileJVMContract fileReader bic cenv <$> traverse getCryptolExpr contract
             res <- case mode of
               VerifyContract -> do
@@ -47,10 +60,10 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc
             setServerVal lemmaName res
             ok
 
-jvmVerify :: VerifyParams JavaType -> Method SAWState OK
+jvmVerify :: VerifyParams JavaType -> Argo.Command SAWState OK
 jvmVerify = jvmVerifyAssume VerifyContract
 
 
-jvmAssume :: AssumeParams JavaType -> Method SAWState OK
+jvmAssume :: AssumeParams JavaType -> Argo.Command SAWState OK
 jvmAssume (AssumeParams className fun contract lemmaName) =
   jvmVerifyAssume AssumeContract (VerifyParams className fun [] False contract (ProofScript []) lemmaName)
diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
index 50ae3419a4..2d76b992e7 100644
--- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
+++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs
@@ -18,15 +18,20 @@ module SAWServer.LLVMCrucibleSetup
   , compileLLVMContract
   ) where
 
-import Control.Lens
-import Control.Monad.IO.Class
+import Control.Lens ( view )
 import Control.Monad.State
+    ( evalStateT,
+      MonadIO(liftIO),
+      MonadState(get, put),
+      MonadTrans(lift),
+      modify' )
 import Data.Aeson (FromJSON(..), withObject, (.:))
 import Data.ByteString (ByteString)
-import Data.Foldable
+import Data.Foldable ( traverse_ )
+import Data.Functor (($>))
 import Data.Map (Map)
 import qualified Data.Map as Map
-import Data.Maybe
+import Data.Maybe ( maybeToList )
 import qualified Data.Text as T
 
 import qualified Cryptol.Parser.AST as P
@@ -51,23 +56,33 @@ import qualified Verifier.SAW.CryptolEnv as CEnv
 import Verifier.SAW.CryptolEnv (CryptolEnv)
 import Verifier.SAW.TypedTerm (TypedTerm)
 
-import Argo
+import qualified Argo
 import qualified Argo.Doc as Doc
 import SAWServer as Server
+    ( ServerName(..),
+      SAWState,
+      SetupStep(..),
+      CrucibleSetupVal(..),
+      SAWTask(LLVMCrucibleSetup),
+      sawTask,
+      pushTask,
+      getHandleAlloc,
+      setServerVal )
 import SAWServer.Data.Contract
+    ( PointsTo(..), Allocated(..), ContractVar(..), Contract(..) )
 import SAWServer.Data.LLVMType (JSONLLVMType, llvmType)
 import SAWServer.Data.SetupValue ()
 import SAWServer.CryptolExpression (getTypedTermOfCExp)
-import SAWServer.Exceptions
-import SAWServer.OK
-import SAWServer.TrackFile
+import SAWServer.Exceptions ( notAtTopLevel, cantLoadLLVMModule )
+import SAWServer.OK ( OK, ok )
+import SAWServer.TrackFile ( trackFile )
 
-startLLVMCrucibleSetup :: StartLLVMCrucibleSetupParams -> Method SAWState OK
+startLLVMCrucibleSetup :: StartLLVMCrucibleSetupParams -> Argo.Command SAWState OK
 startLLVMCrucibleSetup (StartLLVMCrucibleSetupParams n) =
   do pushTask (LLVMCrucibleSetup n [])
      ok
 
-data StartLLVMCrucibleSetupParams
+newtype StartLLVMCrucibleSetupParams
   = StartLLVMCrucibleSetupParams ServerName
 
 instance FromJSON StartLLVMCrucibleSetupParams where
@@ -75,7 +90,7 @@ instance FromJSON StartLLVMCrucibleSetupParams where
     withObject "params for \"SAW/Crucible setup\"" $ \o ->
     StartLLVMCrucibleSetupParams <$> o .: "name"
 
-data ServerSetupVal = Val (CMS.AllLLVM MS.SetupValue)
+newtype ServerSetupVal = Val (CMS.AllLLVM MS.SetupValue)
 
 -- TODO: this is an extra layer of indirection that could be collapsed, but is easy to implement for now.
 compileLLVMContract ::
@@ -108,7 +123,7 @@ interpretLLVMSetup ::
   [SetupStep LLVM.Type] ->
   LLVMCrucibleSetupM ()
 interpretLLVMSetup fileReader bic cenv0 ss =
-  runStateT (traverse_ go ss) (mempty, cenv0) *> pure ()
+  evalStateT (traverse_ go ss) (mempty, cenv0)
   where
     go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= llvm_return
     -- TODO: do we really want two names here?
@@ -211,17 +226,17 @@ llvmLoadModuleDescr :: Doc.Block
 llvmLoadModuleDescr =
   Doc.Paragraph [Doc.Text "Load the specified LLVM module."]
 
-llvmLoadModule :: LLVMLoadModuleParams -> Method SAWState OK
+llvmLoadModule :: LLVMLoadModuleParams -> Argo.Command SAWState OK
 llvmLoadModule (LLVMLoadModuleParams serverName fileName) =
-  do tasks <- view sawTask <$> getState
+  do tasks <- view sawTask <$> Argo.getState
      case tasks of
-       (_:_) -> raise $ notAtTopLevel $ map fst tasks
+       (_:_) -> Argo.raise $ notAtTopLevel $ map fst tasks
        [] ->
          do let ?laxArith = False -- TODO read from config
             halloc <- getHandleAlloc
             loaded <- liftIO (CMS.loadLLVMModule fileName halloc)
             case loaded of
-              Left err -> raise (cantLoadLLVMModule (LLVM.formatError err))
+              Left err -> Argo.raise (cantLoadLLVMModule (LLVM.formatError err))
               Right llvmMod ->
                 do setServerVal serverName llvmMod
                    trackFile fileName
diff --git a/saw-remote-api/src/SAWServer/LLVMVerify.hs b/saw-remote-api/src/SAWServer/LLVMVerify.hs
index d448d047dc..36247f2d86 100644
--- a/saw-remote-api/src/SAWServer/LLVMVerify.hs
+++ b/saw-remote-api/src/SAWServer/LLVMVerify.hs
@@ -10,37 +10,53 @@ module SAWServer.LLVMVerify
   ) where
 
 import Prelude hiding (mod)
-import Control.Lens
+import Control.Lens ( view )
 
 import SAWScript.Crucible.LLVM.Builtins
-import SAWScript.Crucible.LLVM.X86
+    ( llvm_unsafe_assume_spec, llvm_verify )
+import SAWScript.Crucible.LLVM.X86 ( llvm_verify_x86 )
 import SAWScript.Value (rwCryptol)
 
-import Argo
+import qualified Argo
 import qualified Argo.Doc as Doc
 import SAWServer
+    ( SAWState,
+      SAWTask(LLVMCrucibleSetup),
+      sawBIC,
+      sawTask,
+      sawTopLevelRW,
+      pushTask,
+      dropTask,
+      setServerVal,
+      getLLVMModule,
+      getLLVMMethodSpecIR )
 import SAWServer.CryptolExpression (getCryptolExpr)
-import SAWServer.Data.Contract
-import SAWServer.Data.LLVMType
-import SAWServer.Exceptions
-import SAWServer.LLVMCrucibleSetup
-import SAWServer.OK
+import SAWServer.Data.Contract ( ContractMode(..) )
+import SAWServer.Data.LLVMType ( JSONLLVMType )
+import SAWServer.Exceptions ( notAtTopLevel )
+import SAWServer.LLVMCrucibleSetup ( compileLLVMContract )
+import SAWServer.OK ( OK, ok )
 import SAWServer.ProofScript
-import SAWServer.TopLevel
+    ( ProofScript(ProofScript), interpretProofScript )
+import SAWServer.TopLevel ( tl )
 import SAWServer.VerifyCommon
+    ( AssumeParams(AssumeParams),
+      X86VerifyParams(X86VerifyParams),
+      X86Alloc(X86Alloc),
+      VerifyParams(VerifyParams) )
 
-llvmVerifyAssume :: ContractMode -> VerifyParams JSONLLVMType -> Method SAWState OK
+llvmVerifyAssume :: ContractMode -> VerifyParams JSONLLVMType -> Argo.Command SAWState OK
 llvmVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract script lemmaName) =
-  do tasks <- view sawTask <$> getState
+  do tasks <- view sawTask <$> Argo.getState
      case tasks of
-       (_:_) -> raise $ notAtTopLevel $ map fst tasks
+       (_:_) -> Argo.raise $ notAtTopLevel $ map fst tasks
        [] ->
          do pushTask (LLVMCrucibleSetup lemmaName [])
-            state <- getState
+            state <- Argo.getState
             mod <- getLLVMModule modName
             let bic = view sawBIC state
                 cenv = rwCryptol (view sawTopLevelRW state)
-            fileReader <- getFileReader
+            fileReader <- Argo.getFileReader
             setup <- compileLLVMContract fileReader bic cenv <$> traverse getCryptolExpr contract
             res <- case mode of
               VerifyContract -> do
@@ -59,7 +75,7 @@ llvmVerifyDescr :: Doc.Block
 llvmVerifyDescr =
   Doc.Paragraph [Doc.Text "Verify the named LLVM function meets its specification."]
 
-llvmVerify :: VerifyParams JSONLLVMType -> Method SAWState OK
+llvmVerify :: VerifyParams JSONLLVMType -> Argo.Command SAWState OK
 llvmVerify = llvmVerifyAssume VerifyContract
 
 
@@ -70,7 +86,7 @@ llvmAssumeDescr :: Doc.Block
 llvmAssumeDescr =
   Doc.Paragraph [Doc.Text $ "Assume the function meets its specification."]
 
-llvmAssume :: AssumeParams JSONLLVMType -> Method SAWState OK
+llvmAssume :: AssumeParams JSONLLVMType -> Argo.Command SAWState OK
 llvmAssume (AssumeParams modName fun contract lemmaName) =
   llvmVerifyAssume AssumeContract (VerifyParams modName fun [] False contract (ProofScript []) lemmaName)
 
@@ -83,20 +99,20 @@ llvmVerifyX86Descr =
   Doc.Paragraph [ Doc.Text "Verify an x86 function from an ELF file for use as"
                 , Doc.Text " an override in an LLVM verification meets its specification."]
 
-llvmVerifyX86 :: X86VerifyParams JSONLLVMType -> Method SAWState OK
+llvmVerifyX86 :: X86VerifyParams JSONLLVMType -> Argo.Command SAWState OK
 llvmVerifyX86 (X86VerifyParams modName objName fun globals _lemmaNames checkSat contract script lemmaName) =
-  do tasks <- view sawTask <$> getState
+  do tasks <- view sawTask <$> Argo.getState
      case tasks of
-       (_:_) -> raise $ notAtTopLevel $ map fst tasks
+       (_:_) -> Argo.raise $ notAtTopLevel $ map fst tasks
        [] ->
          do pushTask (LLVMCrucibleSetup lemmaName [])
-            state <- getState
+            state <- Argo.getState
             mod <- getLLVMModule modName
             let bic = view  sawBIC state
                 cenv = rwCryptol (view sawTopLevelRW state)
                 allocs = map (\(X86Alloc name size) -> (name, size)) globals
             proofScript <- interpretProofScript script
-            fileReader <- getFileReader
+            fileReader <- Argo.getFileReader
             setup <- compileLLVMContract fileReader bic cenv <$> traverse getCryptolExpr contract
             res <- tl $ llvm_verify_x86 mod objName fun allocs checkSat setup proofScript
             dropTask
diff --git a/saw-remote-api/src/SAWServer/NoParams.hs b/saw-remote-api/src/SAWServer/NoParams.hs
index e79d73fa1c..97198e2a2b 100644
--- a/saw-remote-api/src/SAWServer/NoParams.hs
+++ b/saw-remote-api/src/SAWServer/NoParams.hs
@@ -1,6 +1,7 @@
 module SAWServer.NoParams (NoParams(..)) where
 
 import Data.Aeson
+    ( withObject, object, FromJSON(parseJSON), ToJSON(toJSON) )
 import qualified Argo.Doc as Doc
 
 data NoParams = NoParams
diff --git a/saw-remote-api/src/SAWServer/OK.hs b/saw-remote-api/src/SAWServer/OK.hs
index eed8ea1e84..906881717d 100644
--- a/saw-remote-api/src/SAWServer/OK.hs
+++ b/saw-remote-api/src/SAWServer/OK.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 module SAWServer.OK (OK(..), ok) where
 
-import Data.Aeson
+import Data.Aeson ( ToJSON(toJSON) )
 
 data OK = OK
 
diff --git a/saw-remote-api/src/SAWServer/ProofScript.hs b/saw-remote-api/src/SAWServer/ProofScript.hs
index 9dd21a9a01..8bd9379bf0 100644
--- a/saw-remote-api/src/SAWServer/ProofScript.hs
+++ b/saw-remote-api/src/SAWServer/ProofScript.hs
@@ -9,19 +9,32 @@ module SAWServer.ProofScript
   , proveDescr
   ) where
 
-import Control.Applicative
+import Control.Applicative ( Alternative(empty) )
 import Control.Monad (foldM)
 import Data.Aeson
+    ( (.:),
+      withObject,
+      object,
+      FromJSON(parseJSON),
+      KeyValue((.=)),
+      ToJSON(toJSON) )
 import Data.Text (Text)
 
-import Argo
+import qualified Argo
 import qualified Argo.Doc as Doc
 import qualified SAWScript.Builtins as SB
 import qualified SAWScript.Value as SV
 import SAWServer
-import SAWServer.Exceptions
-import SAWServer.OK
-import SAWServer.TopLevel
+    ( ServerVal(VTerm, VSimpset),
+      ServerName,
+      SAWState,
+      setServerVal,
+      getServerVal,
+      getSimpset,
+      getTerm )
+import SAWServer.Exceptions ( notASimpset )
+import SAWServer.OK ( OK, ok )
+import SAWServer.TopLevel ( tl )
 import Verifier.SAW.Rewriter (addSimp, emptySimpset)
 import Verifier.SAW.TermNet (merge)
 import Verifier.SAW.TypedTerm (TypedTerm(..))
@@ -99,14 +112,14 @@ makeSimpsetDescr :: Doc.Block
 makeSimpsetDescr =
   Doc.Paragraph [Doc.Text "Create a simplification rule set from the given rules."]
 
-makeSimpset :: MakeSimpsetParams -> Method SAWState OK
+makeSimpset :: MakeSimpsetParams -> Argo.Command SAWState OK
 makeSimpset params = do
   let add ss n = do
         v <- getServerVal n
         case v of
           VSimpset ss' -> return (merge ss ss')
           VTerm t -> return (addSimp (ttTerm t) ss)
-          _ -> raise (notASimpset n)
+          _ -> Argo.raise (notASimpset n)
   ss <- foldM add emptySimpset (ssElements params)
   setServerVal (ssResult params) ss
   ok
@@ -151,7 +164,7 @@ proveDescr =
   Doc.Paragraph [ Doc.Text "Attempt to prove the given term representing a"
                 , Doc.Text " theorem, given a proof script context."]
 
-prove :: ProveParams -> Method SAWState ProveResult
+prove :: ProveParams -> Argo.Command SAWState ProveResult
 prove params = do
   t <- getTerm (ppTermName params)
   proofScript <- interpretProofScript (ppScript params)
@@ -160,7 +173,7 @@ prove params = do
     SV.Valid _ -> return ProofValid
     SV.InvalidMulti _  _ -> return ProofInvalid
 
-interpretProofScript :: ProofScript -> Method SAWState (SV.ProofScript SV.SatResult)
+interpretProofScript :: ProofScript -> Argo.Command SAWState (SV.ProofScript SV.SatResult)
 interpretProofScript (ProofScript ts) = go ts
   where go [UseProver ABC]            = return $ SB.proveABC
         go [UseProver (CVC4 unints)]  = return $ SB.proveUnintCVC4 unints
diff --git a/saw-remote-api/src/SAWServer/SaveTerm.hs b/saw-remote-api/src/SAWServer/SaveTerm.hs
index 6201733c23..052ac044ed 100644
--- a/saw-remote-api/src/SAWServer/SaveTerm.hs
+++ b/saw-remote-api/src/SAWServer/SaveTerm.hs
@@ -6,19 +6,19 @@ module SAWServer.SaveTerm
 
 import Data.Aeson (FromJSON(..), withObject, (.:))
 
-import Argo
+import qualified Argo
 import qualified Argo.Doc as Doc
 
-import CryptolServer.Data.Expression
-import SAWServer
-import SAWServer.CryptolExpression
-import SAWServer.OK
+import CryptolServer.Data.Expression ( Expression )
+import SAWServer ( ServerName, SAWState, setServerVal )
+import SAWServer.CryptolExpression ( getTypedTerm )
+import SAWServer.OK ( OK, ok )
 
 saveTermDescr :: Doc.Block
 saveTermDescr =
   Doc.Paragraph [Doc.Text "Save a term to be referenced later by name."]
 
-saveTerm :: SaveTermParams -> Method SAWState OK
+saveTerm :: SaveTermParams -> Argo.Command SAWState OK
 saveTerm (SaveTermParams name e) =
   do setServerVal name =<< getTypedTerm e
      ok
diff --git a/saw-remote-api/src/SAWServer/SetOption.hs b/saw-remote-api/src/SAWServer/SetOption.hs
index 2f29a3b1b7..dc02ce2c5d 100644
--- a/saw-remote-api/src/SAWServer/SetOption.hs
+++ b/saw-remote-api/src/SAWServer/SetOption.hs
@@ -12,21 +12,21 @@ import Data.Aeson.Types (Parser)
 
 import SAWScript.Value
 
-import Argo
+import qualified Argo
 import qualified Argo.Doc as Doc
 
-import SAWServer
-import SAWServer.OK
+import SAWServer ( SAWState, sawTopLevelRW )
+import SAWServer.OK ( OK, ok )
 
 
 setOptionDescr :: Doc.Block
 setOptionDescr =
   Doc.Paragraph [Doc.Text "Set a SAW option in the server."]
 
-setOption :: SetOptionParams -> Method SAWState OK
+setOption :: SetOptionParams -> Argo.Command SAWState OK
 setOption opt =
-  do rw <- view sawTopLevelRW <$> getState
-     let updateRW = modifyState . set sawTopLevelRW
+  do rw <- view sawTopLevelRW <$> Argo.getState
+     let updateRW = Argo.modifyState . set sawTopLevelRW
      case opt of
        EnableLaxArithmetic enabled ->
          updateRW rw { rwLaxArith = enabled }
diff --git a/saw-remote-api/src/SAWServer/Term.hs b/saw-remote-api/src/SAWServer/Term.hs
index 26b39ff4f4..5fd2a6f17b 100644
--- a/saw-remote-api/src/SAWServer/Term.hs
+++ b/saw-remote-api/src/SAWServer/Term.hs
@@ -1,12 +1,13 @@
 {-# LANGUAGE OverloadedStrings #-}
 module SAWServer.Term (JSONModuleName(..)) where
 
-import Control.Applicative
+import Control.Applicative ( Alternative((<|>)) )
 import Data.Aeson as JSON
+    ( withArray, withText, FromJSON(parseJSON), ToJSON(toJSON) )
 import qualified Data.Text as T
 import qualified Data.Vector as V
 
-import Verifier.SAW.Term.Functor
+import Verifier.SAW.Term.Functor ( mkModuleName, ModuleName )
 
 newtype JSONModuleName = JSONModuleName ModuleName
 
diff --git a/saw-remote-api/src/SAWServer/TopLevel.hs b/saw-remote-api/src/SAWServer/TopLevel.hs
index b3c632c1ea..8121edd6f7 100644
--- a/saw-remote-api/src/SAWServer/TopLevel.hs
+++ b/saw-remote-api/src/SAWServer/TopLevel.hs
@@ -2,25 +2,25 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 module SAWServer.TopLevel (tl) where
 
-import Control.Exception
-import Control.Lens
-import Control.Monad.State
+import Control.Exception ( try, SomeException )
+import Control.Lens ( view, set )
+import Control.Monad.State ( MonadIO(liftIO) )
 
-import SAWScript.Value
+import SAWScript.Value ( TopLevel, runTopLevel )
 
-import Argo
-import SAWServer
-import SAWServer.Exceptions
+import qualified Argo
+import SAWServer ( SAWState, sawTopLevelRO, sawTopLevelRW )
+import SAWServer.Exceptions ( verificationException )
 
-tl :: TopLevel a -> Method SAWState a
+tl :: TopLevel a -> Argo.Command SAWState a
 tl act =
-  do st <- getState
+  do st <- Argo.getState
      let ro = view sawTopLevelRO st
          rw = view sawTopLevelRW st
      liftIO (try (runTopLevel act ro rw)) >>=
        \case
          Left (e :: SomeException) ->
-           raise (verificationException e)
+           Argo.raise (verificationException e)
          Right (res, rw') ->
-           do modifyState $ set sawTopLevelRW rw'
+           do Argo.modifyState $ set sawTopLevelRW rw'
               return res
diff --git a/saw-remote-api/src/SAWServer/TrackFile.hs b/saw-remote-api/src/SAWServer/TrackFile.hs
index 5bec3b5cd5..87dbafb6a3 100644
--- a/saw-remote-api/src/SAWServer/TrackFile.hs
+++ b/saw-remote-api/src/SAWServer/TrackFile.hs
@@ -4,21 +4,21 @@ import Control.Lens
 import qualified Data.Map as M
 import qualified Crypto.Hash.Conduit as Hash
 
-import Argo
-import SAWServer
+import qualified Argo
+import SAWServer ( SAWState, trackedFiles )
 
 -- | Add a filepath to the list of filepaths tracked by the server. Any change
 -- to the SHA256 hash of this file will invalidate any cached state which is
 -- causally descended from the moment this method is invoked, unless
 -- @forgetFile@ is used to remove tracking of this file.
-trackFile :: FilePath -> Method SAWState ()
+trackFile :: FilePath -> Argo.Command SAWState ()
 trackFile path =
   do hash <- Hash.hashFile path
-     modifyState $ over trackedFiles (M.insert path hash)
+     Argo.modifyState $ over trackedFiles (M.insert path hash)
 
 -- | Stop tracking a given file. Any state that causally descends from the
 -- moment this method is invoked will not be invalidated by changes to the file
 -- on disk, even if this file was previously tracked via @trackFile@.
-forgetFile :: FilePath -> Method SAWState ()
+forgetFile :: FilePath -> Argo.Command SAWState ()
 forgetFile path =
-  modifyState $ over trackedFiles (M.delete path)
+  Argo.modifyState $ over trackedFiles (M.delete path)
diff --git a/saw-remote-api/src/SAWServer/VerifyCommon.hs b/saw-remote-api/src/SAWServer/VerifyCommon.hs
index e76d1674c4..3a54917738 100644
--- a/saw-remote-api/src/SAWServer/VerifyCommon.hs
+++ b/saw-remote-api/src/SAWServer/VerifyCommon.hs
@@ -11,10 +11,10 @@ import qualified Argo.Doc as Doc
 import Prelude hiding (mod)
 import Data.Aeson (FromJSON(..), withObject, (.:))
 
-import CryptolServer.Data.Expression
-import SAWServer
-import SAWServer.Data.Contract
-import SAWServer.ProofScript
+import CryptolServer.Data.Expression ( Expression )
+import SAWServer ( ServerName )
+import SAWServer.Data.Contract ( Contract )
+import SAWServer.ProofScript ( ProofScript )
 
 data VerifyParams ty =
   VerifyParams