diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,13 @@
+# v0.2
+split `smtlib-backends`'s `Process` module into its own library
+## `Config` datatype
+- move the logger function into it
+- make it an instance of the `Default` typeclass
+## logging
+- move the logger function into the `Config` datatype 
+- don't prefix error messages with `[stderr]`
+## test-suite
+- add usage examples
+- make compatible with `smtlib-backends-0.2`
+## miscellaneous
+- improve documentation
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) Tweag I/O Limited.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+import Distribution.Simple
+
+main = defaultMain
diff --git a/smtlib-backends-process.cabal b/smtlib-backends-process.cabal
new file mode 100644
--- /dev/null
+++ b/smtlib-backends-process.cabal
@@ -0,0 +1,60 @@
+name:               smtlib-backends-process
+version:            0.2
+synopsis:           An SMT-LIB backend running solvers as external processes.
+description:
+  This library implements an SMT-LIB backend (in the sense of the smtlib-backends
+  package) using by running solvers as external processes.
+
+license:            MIT
+license-file:       LICENSE
+author:             Quentin Aristote
+maintainer:         quentin.aristote@tweag.io
+build-type:         Simple
+category:           SMT
+cabal-version:      >=1.10
+extra-source-files: CHANGELOG.md
+
+source-repository head
+  type:     git
+  location: https://github.com/tweag/smtlib-backends
+  subdir:   smtlib-backends-process
+
+source-repository this
+  type:     git
+  location: https://github.com/tweag/smtlib-backends
+  tag:      0.2
+  subdir:   smtlib-backends-process
+
+library
+  hs-source-dirs:   src
+  ghc-options:      -Wall -Wunused-packages
+  exposed-modules:  SMTLIB.Backends.Process
+  other-extensions: Safe
+  build-depends:
+      async            >=2.2.4   && <2.3
+    , base             >=4.14    && <4.17.0
+    , bytestring       >=0.10.12 && <0.11
+    , data-default     >=0.7.1   && <0.8
+    , smtlib-backends  >=0.2     && <0.3
+    , typed-process    >=0.2.10  && <0.3
+
+  default-language: Haskell2010
+
+test-suite test
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   tests
+  main-is:          Main.hs
+  other-modules:    Examples
+  ghc-options:      -threaded -Wall -Wunused-packages
+  build-depends:
+      base
+    , bytestring
+    , data-default
+    , smtlib-backends
+    , smtlib-backends-process
+    , smtlib-backends-tests
+    , tasty
+    , tasty-hunit
+    , typed-process
+
+  default-language: Haskell2010
diff --git a/src/SMTLIB/Backends/Process.hs b/src/SMTLIB/Backends/Process.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLIB/Backends/Process.hs
@@ -0,0 +1,188 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ViewPatterns #-}
+
+-- | A module providing a backend that launches solvers as external processes.
+module SMTLIB.Backends.Process
+  ( Config (..),
+    Handle (..),
+    new,
+    wait,
+    close,
+    with,
+    toBackend,
+  )
+where
+
+import Control.Concurrent.Async (Async, async, cancel)
+import qualified Control.Exception as X
+import Control.Monad (forever)
+import Data.ByteString.Builder
+  ( Builder,
+    byteString,
+    hPutBuilder,
+    toLazyByteString,
+  )
+import qualified Data.ByteString.Char8 as BS
+import qualified Data.ByteString.Lazy.Char8 as LBS
+import Data.Default (Default, def)
+import SMTLIB.Backends (Backend (..))
+import System.Exit (ExitCode)
+import qualified System.IO as IO
+import System.Process.Typed
+  ( Process,
+    getStderr,
+    getStdin,
+    getStdout,
+    mkPipeStreamSpec,
+    setStderr,
+    setStdin,
+    setStdout,
+    startProcess,
+    stopProcess,
+    waitExitCode,
+  )
+import qualified System.Process.Typed as P (proc)
+
+data Config = Config
+  { -- | The command to call to run the solver.
+    exe :: String,
+    -- | Arguments to pass to the solver's command.
+    args :: [String],
+    -- | A function for logging the solver process' messages on stderr and file
+    -- handle exceptions.
+    -- If you want line breaks between each log message, you need to implement
+    -- it yourself, e.g use @'LBS.putStr' . (<> "\n")@.
+    reportError :: LBS.ByteString -> IO ()
+  }
+
+-- | By default, use Z3 as an external process and ignore log messages.
+instance Default Config where
+  -- if you change this, make sure to also update the comment two lines above
+  -- as well as the one in @smtlib-backends-process/tests/Examples.hs@
+  def = Config "z3" ["-in"] $ const $ return ()
+
+data Handle = Handle
+  { -- | The process running the solver.
+    process :: Process IO.Handle IO.Handle IO.Handle,
+    -- | A process reading the solver's error messages and logging them.
+    errorReader :: Async ()
+  }
+
+-- | Run a solver as a process.
+-- Failures relative to terminating the process are logged and discarded.
+new ::
+  -- | The solver process' configuration.
+  Config ->
+  IO Handle
+new config = do
+  solverProcess <-
+    startProcess $
+      setStdin createLoggedPipe $
+        setStdout createLoggedPipe $
+          setStderr createLoggedPipe $
+            P.proc (exe config) (args config)
+  -- log error messages created by the backend
+  solverErrorReader <-
+    async $
+      forever
+        ( do
+            errs <- BS.hGetLine $ getStderr solverProcess
+            reportError' errs
+        )
+        `X.catch` \X.SomeException {} ->
+          return ()
+  return $ Handle solverProcess solverErrorReader
+  where
+    createLoggedPipe =
+      mkPipeStreamSpec $ \_ h -> do
+        IO.hSetBinaryMode h True
+        IO.hSetBuffering h $ IO.BlockBuffering Nothing
+        return
+          ( h,
+            IO.hClose h `X.catch` \ex ->
+              reportError' $ BS.pack $ show (ex :: X.IOException)
+          )
+    reportError' = (reportError config) . LBS.fromStrict
+
+-- | Wait for the process to exit and cleanup its resources.
+wait :: Handle -> IO ExitCode
+wait handle = do
+  cancel $ errorReader handle
+  waitExitCode $ process handle
+
+-- | Terminate the process, wait for it to actually exit and cleanup its resources.
+-- Don't use this if you're manually stopping the solver process by sending an
+-- @(exit)@ command. Use `wait` instead.
+close :: Handle -> IO ()
+close handle = do
+  cancel $ errorReader handle
+  stopProcess $ process handle
+
+-- | Create a solver process, use it to make a computation and stop it.
+-- Don't use this if you're manually stopping the solver process by sending an
+-- @(exit)@ command. Use @\config -> `bracket` (`new` config) `wait`@ instead.
+with ::
+  -- | The solver process' configuration.
+  Config ->
+  -- | The computation to run with the solver process
+  (Handle -> IO a) ->
+  IO a
+with config = X.bracket (new config) close
+
+infixr 5 :<
+
+pattern (:<) :: Char -> BS.ByteString -> BS.ByteString
+pattern c :< rest <- (BS.uncons -> Just (c, rest))
+
+-- | Make the solver process into an SMT-LIB backend.
+toBackend :: Handle -> Backend
+toBackend handle =
+  Backend $ \cmd -> do
+    hPutBuilder (getStdin $ process handle) $ cmd <> "\n"
+    IO.hFlush $ getStdin $ process handle
+    toLazyByteString <$> continueNextLine (scanParen 0) mempty
+  where
+    -- scanParen read lines from the handle's output channel until it has detected
+    -- a complete s-expression, i.e. a well-parenthesized word that may contain
+    -- strings, quoted symbols, and comments
+    -- if we detect a ')' at depth 0 that is not enclosed in a string, a quoted
+    -- symbol or a comment, we give up and return immediately
+    -- see also the SMT-LIB standard v2.6
+    -- https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf#part.2
+    scanParen :: Int -> Builder -> BS.ByteString -> IO Builder
+    scanParen depth acc ('(' :< more) = scanParen (depth + 1) acc more
+    scanParen depth acc ('"' :< more) = do
+      (acc', more') <- string acc more
+      scanParen depth acc' more'
+    scanParen depth acc ('|' :< more) = do
+      (acc', more') <- quotedSymbol acc more
+      scanParen depth acc' more'
+    scanParen depth acc (';' :< _) = continueNextLine (scanParen depth) acc
+    scanParen depth acc (')' :< more)
+      | depth <= 1 = return acc
+      | otherwise = scanParen (depth - 1) acc more
+    scanParen depth acc (_ :< more) = scanParen depth acc more
+    -- mempty case
+    scanParen 0 acc _ = return acc
+    scanParen depth acc _ = continueNextLine (scanParen depth) acc
+
+    string :: Builder -> BS.ByteString -> IO (Builder, BS.ByteString)
+    string acc ('"' :< '"' :< more) = string acc more
+    string acc ('"' :< more) = return (acc, more)
+    string acc (_ :< more) = string acc more
+    -- mempty case
+    string acc _ = continueNextLine string acc
+
+    quotedSymbol :: Builder -> BS.ByteString -> IO (Builder, BS.ByteString)
+    quotedSymbol acc ('|' :< more) = return (acc, more)
+    quotedSymbol acc (_ :< more) = string acc more
+    -- mempty case
+    quotedSymbol acc _ = continueNextLine quotedSymbol acc
+
+    continueNextLine :: (Builder -> BS.ByteString -> IO a) -> Builder -> IO a
+    continueNextLine f acc = do
+      next <- BS.hGetLine $ getStdout $ process handle
+      f (acc <> byteString next) next
diff --git a/tests/Examples.hs b/tests/Examples.hs
new file mode 100644
--- /dev/null
+++ b/tests/Examples.hs
@@ -0,0 +1,85 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Examples (examples) where
+
+import qualified Data.ByteString.Lazy.Char8 as LBS
+import Data.Default (def)
+import SMTLIB.Backends (command, command_, initSolver)
+import qualified SMTLIB.Backends.Process as Process
+import System.Exit (ExitCode (ExitSuccess))
+import System.IO (BufferMode (LineBuffering), hSetBuffering)
+import System.Process.Typed (getStdin)
+import Test.Tasty
+import Test.Tasty.HUnit
+
+-- | The examples for the 'Process' backend (running solvers as external
+-- processes).
+examples :: [TestTree]
+examples =
+  [ testCase "basic use" basicUse,
+    testCase "setting options" setOptions,
+    testCase "exiting manually" manualExit
+  ]
+
+-- | Basic use of the 'Process' backend.
+basicUse :: IO ()
+basicUse =
+  -- 'Process.with' runs a computation using the 'Process' backend
+  Process.with
+    -- the configuration type 'Process.Config' is an instance of the 'Default' class
+    -- we can thus use a default configuration for the backend with the 'def' method
+    -- this default configuration uses Z3 as an external process and disables logging
+    def
+    $ \handle -> do
+      -- first, we make the process handle into an actual backend
+      let backend = Process.toBackend handle
+      -- then, we create a solver out of the backend
+      -- we enable queuing (it's faster !)
+      solver <- initSolver backend True
+      -- we send a basic command to the solver and ignore the response
+      -- we can write the command as a simple string because we have enabled the
+      -- OverloadedStrings pragma
+      _ <- command solver "(get-info :name)"
+      return ()
+
+-- | An example of how to change the default settings of the 'Process' backend.
+setOptions :: IO ()
+setOptions =
+  -- here we use a custom-made configuration
+  let myConfig =
+        Process.Config
+          { Process.exe = "z3",
+            Process.args = ["-in", "solver.timeout=10000"],
+            Process.reportError = LBS.putStr . (`LBS.snoc` '\n')
+          }
+   in Process.with myConfig $ \handle -> do
+        -- since the 'Process' module exposes its 'Handle' datatype entirely, we can also
+        -- change the settings of the underlying process
+        -- you probably won't need to do this as the library already choose these
+        -- settings to ensure the communication with the solvers is as fast as
+        -- possible
+        let p = Process.process handle
+            stdin = getStdin p
+        -- for instance here we change the buffering mode of the process' input channel
+        hSetBuffering stdin LineBuffering
+        -- we can then use the backend as before
+        let backend = Process.toBackend handle
+        solver <- initSolver backend True
+        _ <- command solver "(get-info :name)"
+        return ()
+
+-- | An example of how to close the 'Process' backend's underlying process manually,
+-- instead of relying on 'Process.with' or 'Process.close'.
+manualExit :: IO ()
+manualExit = do
+  -- launch a new process with 'Process.new'
+  handle <- Process.new def
+  let backend = Process.toBackend handle
+  -- here we disable queuing so that we can use 'command_' to ensure the exit
+  -- command will be received successfully
+  solver <- initSolver backend False
+  command_ solver "(exit)"
+  -- 'Process.wait' takes care of cleaning resources and waits for the process to
+  -- exit
+  exitCode <- Process.wait handle
+  assertBool "the solver process didn't exit properly" $ exitCode == ExitSuccess
diff --git a/tests/Main.hs b/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Main.hs
@@ -0,0 +1,15 @@
+import Data.Default (def)
+import Examples (examples)
+import qualified SMTLIB.Backends.Process as Process
+import SMTLIB.Backends.Tests (sources, testBackend)
+import Test.Tasty
+
+main :: IO ()
+main = do
+  defaultMain $
+    testGroup
+      "Tests"
+      [ testBackend "Basic examples" sources $ \todo ->
+          Process.with def $ todo . Process.toBackend,
+        testGroup "API usage examples" examples
+      ]