diff --git a/.hlint.yaml b/.hlint.yaml
index 7564743..4ec5cbb 100644
--- a/.hlint.yaml
+++ b/.hlint.yaml
@@ -1,3 +1,10 @@
 - arguments: [ -XTypeApplications ]
 
 - ignore: { name: Eta reduce }
+# https://github.com/ndmitchell/hlint/issues/186
+- ignore:
+    name: Unused LANGUAGE pragma
+    within:
+    - Test.Network.Gossip.Broadcast
+    - Test.Network.Gossip.Membership
+    - Test.Network.Gossip.Membership.StateMachine
diff --git a/.stylish-haskell.yaml b/.stylish-haskell.yaml
index da36aa8..9b68a78 100644
--- a/.stylish-haskell.yaml
+++ b/.stylish-haskell.yaml
@@ -184,6 +184,8 @@ language_extensions:
   - DeriveFunctor
   - DeriveGeneric
   - DeriveTraversable
+  - DerivingStrategies
+  - DerivingVia
   - FlexibleContexts
   - FlexibleInstances
   - FunctionalDependencies
diff --git a/gossip.cabal b/gossip.cabal
index ff75f88..4076277 100644
--- a/gossip.cabal
+++ b/gossip.cabal
@@ -104,6 +104,7 @@ test-suite tests
 
     build-depends:
         algebraic-graphs == 0.2.*
+      , generic-lens
       , gossip
       , hashable
       , hedgehog
@@ -118,6 +119,7 @@ test-suite tests
         Test.Network.Gossip.Gen
         Test.Network.Gossip.Helpers
         Test.Network.Gossip.Membership
+        Test.Network.Gossip.Membership.StateMachine
 
     ghc-options:
         -threaded
diff --git a/src/Network/Gossip/HyParView.hs b/src/Network/Gossip/HyParView.hs
index 0090799..8d5d391 100644
--- a/src/Network/Gossip/HyParView.hs
+++ b/src/Network/Gossip/HyParView.hs
@@ -109,7 +109,17 @@ data Connection n = Connection
 data Peers n = Peers
     { active  :: HashSet n
     , passive :: HashSet n
-    }
+    } deriving (Eq, Show, Generic)
+
+instance (Eq n, Hashable n) => Semigroup (Peers n) where
+    a <> b = Peers
+        { active  = active  a <> active  b
+        , passive = passive a <> passive b
+        }
+
+instance (Eq n, Hashable n) => Monoid (Peers n) where
+    mempty  = Peers mempty mempty
+    mappend = (<>)
 
 -- TODO: stm containers
 data Env n = Env
diff --git a/test/Main.hs b/test/Main.hs
index ff6602e..420e232 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -2,6 +2,7 @@ module Main (main) where
 
 import qualified Test.Network.Gossip.Broadcast as Broadcast
 import qualified Test.Network.Gossip.Membership as Membership
+import qualified Test.Network.Gossip.Membership.StateMachine as Membership.State
 
 import           Control.Monad (unless)
 import           System.Exit (exitFailure)
@@ -12,6 +13,7 @@ main = do
         and <$> sequence
             [ Broadcast.tests
             , Membership.tests
+            , Membership.State.tests
             ]
 
     unless success exitFailure
diff --git a/test/Test/Network/Gossip/Broadcast.hs b/test/Test/Network/Gossip/Broadcast.hs
index f8ebaa2..090688b 100644
--- a/test/Test/Network/Gossip/Broadcast.hs
+++ b/test/Test/Network/Gossip/Broadcast.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TemplateHaskell   #-}
 
 module Test.Network.Gossip.Broadcast (tests) where
 
@@ -37,13 +38,10 @@ import qualified Hedgehog.Gen as Gen
 import qualified Hedgehog.Range as Range
 
 tests :: IO Bool
-tests = checkParallel $ Group "Gossip.Broadcast"
-    [ ("prop_atomic_connected",      propAtomicConnected)
-    , ("prop_atomic_network_delays", propAtomicNetworkDelays)
-    ]
+tests = checkParallel $$discover
 
-propAtomicConnected :: Property
-propAtomicConnected = property $ do
+prop_atomicConnected :: Property
+prop_atomicConnected = property $ do
     seed   <- forAll $ Gen.prune Gen.splitMixSeed
     boot   <- forAll $ Gen.connectedContacts Gen.defaultNetworkBounds
     links  <-
@@ -52,8 +50,8 @@ propAtomicConnected = property $ do
     bcasts <- forAll $ genBroadcasts boot
     atomicBroadcast (seedSMGen' seed) boot links bcasts
 
-propAtomicNetworkDelays :: Property
-propAtomicNetworkDelays = property $ do
+prop_atomicNetworkDelays :: Property
+prop_atomicNetworkDelays = property $ do
     seed   <- forAll $ Gen.prune Gen.splitMixSeed
     boot   <- forAll $ Gen.connectedContacts Gen.defaultNetworkBounds
     links  <-
diff --git a/test/Test/Network/Gossip/Gen.hs b/test/Test/Network/Gossip/Gen.hs
index 79d00ee..fde3e59 100644
--- a/test/Test/Network/Gossip/Gen.hs
+++ b/test/Test/Network/Gossip/Gen.hs
@@ -1,5 +1,9 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeFamilies               #-}
+
 module Test.Network.Gossip.Gen
-    ( MockNodeId
+    ( MockPeer (..)
+    , MockNodeId
     , Contacts
     , SplitMixSeed
     , LinkState (..)
@@ -9,6 +13,9 @@ module Test.Network.Gossip.Gen
     , NetworkBounds
     , defaultNetworkBounds
 
+    , mockPeer
+    , nodeId
+
     , connectedContacts
     , disconnectedContacts
     , circularContacts
@@ -21,6 +28,8 @@ module Test.Network.Gossip.Gen
     )
 where
 
+import           Network.Gossip.HyParView (HasPeerAddr(..), HasPeerNodeId(..))
+
 import qualified Algebra.Graph.Class as Alga
 import           Algebra.Graph.Relation.Symmetric
                  ( SymmetricRelation
@@ -30,11 +39,15 @@ import           Algebra.Graph.Relation.Symmetric
 import qualified Algebra.Graph.ToGraph as Alga
 import           Control.Applicative (liftA2)
 import           Data.Bifunctor (second)
+import           Data.Coerce (coerce)
 import qualified Data.Graph as Graph
+import           Data.Hashable (Hashable)
 import           Data.List (uncons, unfoldr)
+import           Data.Maybe (fromMaybe)
 import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Word (Word16, Word64)
+import           Lens.Micro (lens)
 
 import           Hedgehog
 import qualified Hedgehog.Gen as Gen
@@ -45,6 +58,19 @@ import qualified Test.QuickCheck.Hedgehog as Gen
 
 -- Types -----------------------------------------------------------------------
 
+newtype MockPeer = MockPeer MockNodeId
+    deriving (Eq, Show, Hashable)
+
+instance HasPeerNodeId MockPeer where
+    type NodeId MockPeer = MockNodeId
+    peerNodeId = lens coerce (const coerce)
+    {-# INLINE peerNodeId #-}
+
+instance HasPeerAddr MockPeer where
+    type Addr MockPeer = MockNodeId
+    peerAddr = lens coerce (const coerce)
+    {-# INLINE peerAddr #-}
+
 type MockNodeId   = Word16
 type Contacts     = [(MockNodeId, [MockNodeId])]
 type SplitMixSeed = (Word64, Word64)
@@ -79,6 +105,12 @@ defaultNetworkBounds = NetworkBounds
 
 -- Generators ------------------------------------------------------------------
 
+mockPeer :: MonadGen m => Maybe Int -> m MockPeer
+mockPeer maxPeers = MockPeer <$> nodeId (fromMaybe maxBound maxPeers)
+
+nodeId :: MonadGen m => Int -> m MockNodeId
+nodeId maxNodes = Gen.word16 (Range.constant 0 (fromIntegral $ maxNodes - 1))
+
 ---- Contacts ------------------------------------------------------------------
 
 connectedContacts :: MonadGen m => NetworkBounds -> m Contacts
@@ -170,6 +202,3 @@ nodeIds :: MonadGen m => NetworkBounds -> m (Set MockNodeId)
 nodeIds NetworkBounds{..} =
     Gen.set (Range.constantFrom netMinNodes netMinNodes netMaxContacts)
             (nodeId netMaxNodes)
-
-nodeId :: MonadGen m => Int -> m MockNodeId
-nodeId maxNodes = Gen.word16 (Range.constant 0 (fromIntegral $ maxNodes - 1))
diff --git a/test/Test/Network/Gossip/Membership.hs b/test/Test/Network/Gossip/Membership.hs
index 342b087..9cbf6d6 100644
--- a/test/Test/Network/Gossip/Membership.hs
+++ b/test/Test/Network/Gossip/Membership.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE OverloadedStrings          #-}
+{-# LANGUAGE TemplateHaskell            #-}
 {-# LANGUAGE TypeFamilies               #-}
 
 module Test.Network.Gossip.Membership (tests) where
@@ -11,6 +12,7 @@ import           Test.Network.Gossip.Gen
                  , InfiniteListOf(..)
                  , LinkState(..)
                  , MockNodeId
+                 , MockPeer(..)
                  , SplitMixSeed
                  , renderInf
                  )
@@ -21,16 +23,13 @@ import qualified Algebra.Graph.AdjacencyMap as Alga
 import           Control.Concurrent (threadDelay)
 import           Control.Monad.Trans.Class (lift)
 import           Data.Bifunctor (second)
-import           Data.Coerce (coerce)
 import           Data.Foldable (for_)
-import           Data.Hashable (Hashable)
 import qualified Data.HashSet as Set
 import           Data.IORef (IORef, atomicModifyIORef', newIORef)
 import           Data.List (uncons)
 import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import           Data.Traversable (for)
-import           Lens.Micro (lens)
 import           Lens.Micro.Extras (view)
 import           System.Random (randomR, split)
 import           System.Random.SplitMix (SMGen, seedSMGen')
@@ -38,19 +37,6 @@ import           System.Random.SplitMix (SMGen, seedSMGen')
 import           Hedgehog hiding (eval)
 import qualified Hedgehog.Gen as Gen
 
-newtype MockPeer = MockPeer MockNodeId
-    deriving (Eq, Hashable)
-
-instance HasPeerNodeId MockPeer where
-    type NodeId MockPeer = MockNodeId
-    peerNodeId = lens coerce (const coerce)
-    {-# INLINE peerNodeId #-}
-
-instance HasPeerAddr MockPeer where
-    type Addr MockPeer = MockNodeId
-    peerAddr = lens coerce (const coerce)
-    {-# INLINE peerAddr #-}
-
 data Network = Network
     { netNodes     :: Map MockNodeId Node
     , netTaskQueue :: TaskQueue
@@ -61,15 +47,10 @@ data Network = Network
 newtype Node = Node { nodeEnv :: Env MockPeer }
 
 tests :: IO Bool
-tests = checkParallel $ Group "Gossip.Membership"
-    [ ("prop_disconnected",       propDisconnected)
-    , ("prop_circular_connected", propCircularConnected)
-    , ("prop_connected",          propConnected)
-    , ("prop_network_delays",     propNetworkDelays)
-    ]
-
-propDisconnected :: Property
-propDisconnected = property $ do
+tests = checkParallel $$discover
+
+prop_disconnected :: Property
+prop_disconnected = property $ do
     seed  <- forAll Gen.splitMixSeed
     boot  <- forAll $ Gen.disconnectedContacts Gen.defaultNetworkBounds
     links <-
@@ -77,8 +58,8 @@ propDisconnected = property $ do
             Gen.prune $ Gen.infiniteListOf (pure Fast)
     activeDisconnected seed boot links
 
-propCircularConnected :: Property
-propCircularConnected = property $ do
+prop_circularConnected :: Property
+prop_circularConnected = property $ do
     seed  <- forAll Gen.splitMixSeed
     boot  <- forAll $ Gen.circularContacts Gen.defaultNetworkBounds
     links <-
@@ -86,8 +67,8 @@ propCircularConnected = property $ do
             Gen.prune $ Gen.infiniteListOf (pure Fast)
     activeConnected seed boot links
 
-propConnected :: Property
-propConnected = property $ do
+prop_connected :: Property
+prop_connected = property $ do
     seed  <- forAll Gen.splitMixSeed
     boot  <- forAll $ Gen.connectedContacts Gen.defaultNetworkBounds
     links <-
@@ -95,8 +76,8 @@ propConnected = property $ do
             Gen.prune $ Gen.infiniteListOf (pure Fast)
     activeConnected seed boot links
 
-propNetworkDelays :: Property
-propNetworkDelays = property $ do
+prop_networkDelays :: Property
+prop_networkDelays = property $ do
     seed  <- forAll Gen.splitMixSeed
     boot  <- forAll $ Gen.connectedContacts Gen.defaultNetworkBounds
     links <-
@@ -116,7 +97,7 @@ activeConnected seed boot links = do
     annotateShow $ passiveNetwork peers
     assert $ isConnected (activeNetwork peers)
 
--- | Like 'propActiveConnected', but assert that the network converges to a
+-- | Like 'activeConnected', but assert that the network converges to a
 -- disconnected state.
 --
 -- This exists to suppress output which 'Test.Tasty.ExpectedFailure.expectFail'
diff --git a/test/Test/Network/Gossip/Membership/StateMachine.hs b/test/Test/Network/Gossip/Membership/StateMachine.hs
new file mode 100644
index 0000000..8f1bff3
--- /dev/null
+++ b/test/Test/Network/Gossip/Membership/StateMachine.hs
@@ -0,0 +1,162 @@
+{-# LANGUAGE DataKinds                  #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE KindSignatures             #-}
+{-# LANGUAGE TemplateHaskell            #-}
+
+module Test.Network.Gossip.Membership.StateMachine (tests) where
+
+import qualified Network.Gossip.HyParView as Impl
+
+import           Control.Monad.IO.Class
+import           Data.Generics.Product
+import           Data.HashSet (HashSet)
+import qualified Data.HashSet as Set
+import           GHC.Generics (Generic)
+import           Lens.Micro (Lens', set)
+import           Lens.Micro.Extras (view)
+import           System.Random.SplitMix (seedSMGen')
+
+import           Hedgehog hiding (eval)
+import qualified Hedgehog.Gen as Gen
+import qualified Hedgehog.Range as Range
+import           Test.Network.Gossip.Gen (MockNodeId, MockPeer(..))
+import qualified Test.Network.Gossip.Gen as Gen
+
+
+tests :: IO Bool
+tests = checkParallel $$discover
+
+data Model (v :: * -> *) = Model
+    { self  :: MockPeer
+    , peers :: Maybe (Var (Impl.Peers MockPeer) v)
+    } deriving Generic
+
+active, passive :: Lens' (Impl.Peers MockPeer) (HashSet MockPeer)
+active  = field @"active"
+passive = field @"passive"
+
+initialState :: MockPeer -> Model v
+initialState self = Model self Nothing
+
+-- Join ------------------------------------------------------------------------
+
+newtype Join (v :: * -> *) = Join MockNodeId
+    deriving (Eq, Show)
+
+instance HTraversable Join where
+    htraverse _ (Join nid) = pure $ Join nid
+
+cmdJoin
+    :: MonadGen n
+    => (MockNodeId -> m (Impl.Peers MockPeer))
+    -> Command n m Model
+cmdJoin run =
+    let
+        gen Model { self } =
+            Just . fmap Join
+                 . Gen.filter (/= view Impl.peerNodeId self)
+                 $ Gen.nodeId maxBound
+
+        exe (Join nid) = run nid
+     in
+        Command gen exe
+            [ Update $ \s _ out ->
+                set (field @"peers") (Just out) s
+
+            , Ensure $ \_ after (Join nid) out ->
+                let
+                    peer   = MockPeer nid
+                    peers' = concrete <$> peers after
+                 in
+                    case peers' of
+                        Nothing -> failure
+                        Just ps -> do
+                            ps === out
+                            assert $ Set.member peer $ view active ps
+            ]
+
+-- Disconnect ------------------------------------------------------------------
+
+newtype Disconnect (v :: * -> *) = Disconnect MockNodeId
+    deriving (Eq, Show)
+
+instance HTraversable Disconnect where
+    htraverse _ (Disconnect nid) = pure $ Disconnect nid
+
+cmdDisconnect
+    :: MonadGen n
+    => (MockNodeId -> m (Impl.Peers MockPeer))
+    -> Command n m Model
+cmdDisconnect run =
+    let
+        gen Model { self } =
+            Just . fmap Disconnect
+                 . Gen.filter (/= view Impl.peerNodeId self)
+                 $ Gen.nodeId maxBound
+
+        exe (Disconnect nid) = run nid
+     in
+        Command gen exe
+            [ Update $ \s _ out ->
+                set (field @"peers") (Just out) s
+
+            , Ensure $ \_ after (Disconnect nid) out ->
+                let
+                    peer = MockPeer nid
+                    peers' = concrete <$> peers after
+                 in
+                    case peers' of
+                        Nothing -> failure
+                        Just ps -> do
+                            ps === out
+                            assert $       Set.member peer $ view passive ps
+                            assert $ not $ Set.member peer $ view active  ps
+            ]
+
+--------------------------------------------------------------------------------
+
+prop_singleNode :: Property
+prop_singleNode = property $ do
+    rng     <- seedSMGen' <$> forAll Gen.splitMixSeed
+    self    <- forAll $ Gen.mockPeer Nothing
+    nenv    <- liftIO $ Impl.new self Impl.defaultConfig rng
+    actions <- forAll $
+        Gen.sequential (Range.linear 1 100) (initialState self)
+            [ cmdJoin $ runJoin nenv
+            , cmdDisconnect $ runDisconnect nenv
+            ]
+    executeSequential (initialState self) actions
+  where
+    runJoin nenv nid = liftIO . runSingleNode nenv $ do
+        Impl.receive Impl.RPC
+            { Impl.rpcSender    = MockPeer nid
+            , Impl.rpcRecipient = Impl.envSelf nenv
+            , Impl.rpcPayload   = Impl.Join
+            }
+        Impl.getPeers'
+
+    runDisconnect nenv nid = liftIO . runSingleNode nenv $ do
+        Impl.receive Impl.RPC
+            { Impl.rpcSender    = MockPeer nid
+            , Impl.rpcRecipient = Impl.envSelf nenv
+            , Impl.rpcPayload   = Impl.Disconnect
+            }
+        Impl.getPeers'
+
+runSingleNode :: Impl.Env MockPeer -> Impl.HyParView MockPeer a -> IO a
+runSingleNode env ma = Impl.runHyParView env ma >>= eval
+  where
+    eval = \case
+        Impl.ConnectionOpen addr _ k ->
+            k (Right (mkConn (MockPeer addr))) >>= eval
+
+        Impl.SendAdHoc    _ k -> k >>= eval
+        Impl.NeighborUp   _ k -> k >>= eval
+        Impl.NeighborDown _ k -> k >>= eval
+        Impl.Done a           -> pure a
+
+    mkConn to' = Impl.Connection
+        { Impl.connPeer  = to'
+        , Impl.connSend  = const $ pure ()
+        , Impl.connClose = pure ()
+        }