diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,8 @@
+2026-05-07
+        * Version bump (4.7.1). (#730)
+        * Add stream analysis module. (#726)
+        * Add state machine module. (#728)
+
 2026-03-07
         * Version bump (4.7). (#714)
 
diff --git a/copilot-libraries.cabal b/copilot-libraries.cabal
--- a/copilot-libraries.cabal
+++ b/copilot-libraries.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-libraries
-version:             4.7
+version:             4.7.1
 synopsis:            Libraries for the Copilot language.
 description:
   Libraries for the Copilot language.
@@ -41,13 +41,15 @@
                , containers       >= 0.4 && < 0.9
                , mtl              >= 2.0 && < 2.4
                , parsec           >= 2.0 && < 3.2
-               , copilot-language >= 4.7 && < 4.8
+               , copilot-language >= 4.7.1 && < 4.8
 
   exposed-modules:
-      Copilot.Library.Libraries
+      Copilot.Library.Analysis
+    , Copilot.Library.Libraries
     , Copilot.Library.Clocks
     , Copilot.Library.LTL
     , Copilot.Library.PTLTL
+    , Copilot.Library.StateMachines
     , Copilot.Library.Statistics
     , Copilot.Library.RegExp
     , Copilot.Library.Utils
diff --git a/src/Copilot/Library/Analysis.hs b/src/Copilot/Library/Analysis.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Library/Analysis.hs
@@ -0,0 +1,23 @@
+-- | Formally analyze streams.
+module Copilot.Library.Analysis
+    ( triviallyTrue
+    , triviallyFalse
+    )
+  where
+
+-- External imports.
+import Prelude hiding (not)
+
+-- Internal imports.
+import Copilot.Language      (Stream, forAll, not)
+import Copilot.Language.Spec (Prop, Universal)
+
+-- | Property that captures whether a stream is trivially true, meaning that
+-- there is no way to make it false.
+triviallyTrue :: Stream Bool -> Prop Universal
+triviallyTrue = forAll
+
+-- | Property that captures whether a stream is trivially false, meaning that
+-- there is no way to make it true.
+triviallyFalse :: Stream Bool -> Prop Universal
+triviallyFalse = triviallyTrue . not
diff --git a/src/Copilot/Library/StateMachines.hs b/src/Copilot/Library/StateMachines.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Library/StateMachines.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+-- | Simulate state machines using streams.
+module Copilot.Library.StateMachines where
+
+import Copilot.Language (Stream, Typed, constant, ifThenElse, (&&), (++), (==))
+import Prelude          hiding ((&&), (++), (==))
+
+-- | A definition of a state machine where some elements are defined
+-- as streams.
+--
+-- A state machine is defined by an initial state, a final state, a no
+-- transition stream (true when tere is no input coming in), a list of
+-- transitions, and a bad state.
+type StateMachine a = (a, a, Stream Bool, [(a, Stream Bool, a)], a)
+
+-- | Produce a stream that, at any given time, contains the current state of
+-- the state machine.
+stateMachine :: forall a . (Eq a, Typed a) => StateMachine a -> Stream a
+stateMachine (initial, final, noInputData, transitions, bad) = state
+  where
+    state         = ifThenElses transitions
+    previousState = [initial] ++ state
+
+    ifThenElses :: [(a, Stream Bool, a)] -> Stream a
+    ifThenElses [] =
+      ifThenElse (previousState == constant final && noInputData)
+        (constant final)
+        (constant bad)
+
+    ifThenElses ((s1, i, s2):ss) =
+      ifThenElse
+        (previousState == constant s1 && i)
+        (constant s2)
+        (ifThenElses ss)
+
+-- | Produce a stream that, at any given time, contains the current state of
+-- the state machine as the numeric representation of an enum.
+stateMachineEnum :: (Eq b, Typed b, Num b, Enum a)
+                 => StateMachine a
+                 -> Stream b
+stateMachineEnum (initial, final, noInputData, transitions, bad) =
+    stateMachine (fe initial, fe final, noInputData, transitionsE, fe bad)
+  where
+    transitionsE = map (\(s1, t, s2) -> (fe s1, t, fe s2)) transitions
+    fe           = fromIntegral . fromEnum