diff --git a/spectacle.cabal b/spectacle.cabal
index 43edf7a..491614e 100644
--- a/spectacle.cabal
+++ b/spectacle.cabal
@@ -1,7 +1,7 @@
 cabal-version:       2.4
 
 name:                spectacle
-version:             0.1.0
+version:             1.0.0
 category:            Testing, Concurrency
 synopsis:            Embedded specification language & model checker in Haskell.
 description:
diff --git a/src/Control/Applicative/Day.hs b/src/Control/Applicative/Day.hs
index 304941f..95ccf7a 100644
--- a/src/Control/Applicative/Day.hs
+++ b/src/Control/Applicative/Day.hs
@@ -8,7 +8,7 @@
 --
 -- 2. "Notions of Computations as Monoids" <https://arxiv.org/abs/1406.4823>
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Control.Applicative.Day
   ( Day (Day),
     getDay,
@@ -30,12 +30,12 @@ wrapDay ma = Day \mx ->
   ma >>= \case
     Day k -> k mx
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Functor f => Functor (Day f) where
   fmap f (Day xs) = Day (fmap (first f) . xs)
   {-# INLINE fmap #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Functor f => Applicative (Day f) where
   pure x = Day (fmap (x,))
   {-# INLINE pure #-}
diff --git a/src/Control/Applicative/Phases.hs b/src/Control/Applicative/Phases.hs
index f659e66..59e5fbd 100644
--- a/src/Control/Applicative/Phases.hs
+++ b/src/Control/Applicative/Phases.hs
@@ -6,7 +6,7 @@
 --
 -- 2. <https://github.com/rampion/tree-traversals>
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Control.Applicative.Phases
   ( Phases (Here, There),
     lowerPhases,
@@ -27,7 +27,7 @@ import Data.Kind (Type)
 -- effects of the underlying @f@. The 'Here' constructor apply effects immediately and 'There' constructors
 -- incrementally delay effects.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data Phases :: (Type -> Type) -> Type -> Type where
   Here :: a -> Phases f a
   There :: (a -> b -> c) -> f a -> Phases f b -> Phases f c
@@ -43,13 +43,13 @@ liftPhases :: Monad f => Phases f (f a) -> Phases f a
 liftPhases (Here x) = There const x (pure ())
 liftPhases (There f x xs) = There const (x >>= \x' -> lowerPhases xs >>= f x') xs
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Functor (Phases f) where
   fmap f (Here x) = Here (f x)
   fmap f (There op x xs) = There (\y ys -> f (y `op` ys)) x xs
   {-# INLINE fmap #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Applicative f => Applicative (Phases f) where
   pure = Here
   {-# INLINE pure #-}
diff --git a/src/Control/Applicative/Queue.hs b/src/Control/Applicative/Queue.hs
index 95543cf..7002726 100644
--- a/src/Control/Applicative/Queue.hs
+++ b/src/Control/Applicative/Queue.hs
@@ -2,7 +2,7 @@
 
 -- | Effect queues.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Control.Applicative.Queue
   ( Queue,
     runQueue,
diff --git a/src/Control/Comonad/Tape.hs b/src/Control/Comonad/Tape.hs
index 674c64c..e09fdf6 100644
--- a/src/Control/Comonad/Tape.hs
+++ b/src/Control/Comonad/Tape.hs
@@ -28,17 +28,17 @@ import qualified Data.Sequence as Seq
 data Tape a = Tape {before :: Seq a, focus :: a, after :: Seq a}
   deriving (Eq, Functor, Show)
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Foldable Tape where
   foldr cons nil = foldr cons nil . toSeq
   {-# INLINE foldr #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Traversable Tape where
   traverse f (Tape lower x upper) = Tape <$> traverse f lower <*> f x <*> traverse f upper
   {-# INLINE traverse #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Comonad Tape where
   extract (Tape _ x _) = x
   {-# INLINE extract #-}
@@ -49,7 +49,7 @@ instance Comonad Tape where
   extend f tp = case duplicate tp of
     Tape ls x us -> Tape (f <$> ls) (f x) (f <$> us)
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance ComonadStore Int Tape where
   pos (Tape lw _ _) = length lw
   {-# INLINE pos #-}
@@ -70,14 +70,14 @@ instance ComonadStore Int Tape where
 
 -- | /O(1)/, @'viewl' xs@ constructs a 'Tape' by viewing @xs@ from the left, if it is nonempty.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 viewl :: Seq a -> Maybe (Tape a)
 viewl Empty = Nothing
 viewl (x :<| upper) = Just (Tape mempty x upper)
 
 -- | /O(1)/, @'viewl' xs@ constructs a 'Tape' by viewing @xs@ from the left, if it is nonempty.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 viewr :: Seq a -> Maybe (Tape a)
 viewr Empty = Nothing
 viewr (lower :|> x) = Just (Tape lower x mempty)
@@ -85,7 +85,7 @@ viewr (lower :|> x) = Just (Tape lower x mempty)
 -- | /O(log n)/, @'viewAt' i xs@ constructs a 'Tape' focusing the ith element of @xs@, if it is nonempty. @i@ is
 -- clamped to the interval [0, i).
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 viewAt :: Int -> Seq a -> Maybe (Tape a)
 viewAt i xs =
   case Seq.splitAt i xs of
diff --git a/src/Control/Hyper.hs b/src/Control/Hyper.hs
index 142611a..7e5cd10 100644
--- a/src/Control/Hyper.hs
+++ b/src/Control/Hyper.hs
@@ -5,7 +5,7 @@
 
 -- | Hyperfunction transformer.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Control.Hyper
   ( HyperM (HyperM, invokeM),
   )
@@ -21,7 +21,7 @@ import Data.Kind (Type)
 newtype HyperM :: (Type -> Type) -> Type -> Type -> Type where
   HyperM :: {invokeM :: m ((HyperM m a b -> a) -> b)} -> HyperM m a b
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Monad m => MonadZip (LogicT m) where
   mzipWith op (LogicT f) (LogicT g) = LogicT \cons nil ->
     let fs x xs = pure (\k -> k (HyperM xs) x)
diff --git a/src/Control/Mealy.hs b/src/Control/Mealy.hs
index cc79fa1..6c8fa63 100644
--- a/src/Control/Mealy.hs
+++ b/src/Control/Mealy.hs
@@ -2,7 +2,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Control.Mealy
   ( -- * Mealy Machines
     Mealy,
@@ -39,17 +39,17 @@ type Mealy = MealyM Identity
 runMealy :: Mealy a b -> a -> (b, Mealy a b)
 runMealy (MealyM k) x = runIdentity (k x)
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance (Applicative m, Semigroup b) => Semigroup (MealyM m a b) where
   MealyM f <> MealyM g = MealyM \x -> liftA2 (<>) (f x) (g x)
   {-# INLINE (<>) #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance (Applicative m, Monoid b) => Monoid (MealyM m a b) where
   mempty = MealyM \_ -> pure mempty
   {-# INLINE mempty #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Applicative m => Applicative (MealyM m a) where
   pure x = MealyM \_ -> pure (x, pure x)
   {-# INLINE pure #-}
diff --git a/src/Control/Monad/Levels.hs b/src/Control/Monad/Levels.hs
index 4ca23e9..edd7d90 100644
--- a/src/Control/Monad/Levels.hs
+++ b/src/Control/Monad/Levels.hs
@@ -1,6 +1,6 @@
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Control.Monad.Levels
   ( -- * Levels
     Levels,
diff --git a/src/Control/Monad/Levels/Internal.hs b/src/Control/Monad/Levels/Internal.hs
index 27af2da..054977e 100644
--- a/src/Control/Monad/Levels/Internal.hs
+++ b/src/Control/Monad/Levels/Internal.hs
@@ -7,7 +7,7 @@
 --
 -- 1. Donnacha Oisín Kidney, Nicolas Wu. 2021. Algebras for Weighted Search.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Control.Monad.Levels.Internal
   ( -- * Levels
     Levels,
@@ -42,12 +42,12 @@ type Levels = LevelsT Identity
 runLevels :: Levels a -> (Bag a -> b -> b) -> b -> b
 runLevels (LevelsT k) cons nil = runIdentity (k (fmap . cons) (pure nil))
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Foldable Levels where
   foldMap f m = runLevels m (mappend . foldMap f) mempty
   {-# INLINE foldMap #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Traversable Levels where
   traverse f m = runLevels m (liftA2 (<|>) . fmap foldAlt . traverse f) (pure empty)
 
@@ -58,7 +58,7 @@ newtype LevelsT :: (Type -> Type) -> Type -> Type where
 
 -- | Constructs a 'LevelsT' with a single level, the monoid provided.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 foldAlt :: Foldable m => m a -> LevelsT f a
 foldAlt xs = LevelsT \cons nil -> cons (foldr Bag.cons Bag.empty xs) nil
 
@@ -68,12 +68,12 @@ liftLevelsT xs = LevelsT (\cons nil -> xs >>= \xs' -> runLevelsT xs' cons nil)
 wrapLevelsT :: Monad m => m (LevelsT m a) -> LevelsT m a
 wrapLevelsT xs = LevelsT (\cons nil -> cons None (xs >>= \xs' -> runLevelsT xs' cons nil))
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Functor (LevelsT m) where
   fmap f (LevelsT g) = LevelsT \cons nil -> g (cons . fmap f) nil
   {-# INLINE fmap #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Monad m => Applicative (LevelsT m) where
   pure x = LevelsT \cons nil -> cons (Bag.singleton x) nil
   {-# INLINE pure #-}
@@ -82,12 +82,12 @@ instance Monad m => Applicative (LevelsT m) where
   (<*>) = ap
   {-# INLINE (<*>) #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Monad m => Monad (LevelsT m) where
   LevelsT m >>= k = liftLevelsT (m (\x xs -> pure (foldr ((<|>) . k) (wrapLevelsT xs) x)) (pure empty))
   {-# INLINE (>>=) #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Monad m => Alternative (LevelsT m) where
   empty = LevelsT \_ nil -> nil
   {-# INLINE empty #-}
@@ -104,17 +104,17 @@ instance Monad m => Alternative (LevelsT m) where
      in f fcons fnil >>= (g gcon (pure gnil) >>=)
   {-# INLINE (<|>) #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance MonadTrans LevelsT where
   lift m = LevelsT \cons nil -> m >>= (`cons` nil) . Bag.singleton
   {-# INLINE lift #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance MonadState s m => MonadState s (LevelsT m) where
   state = lift . state
   {-# INLINE state #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance MonadReader r m => MonadReader r (LevelsT m) where
   reader = lift . reader
   {-# INLINE reader #-}
@@ -123,7 +123,7 @@ instance MonadReader r m => MonadReader r (LevelsT m) where
     local f (g cons nil)
   {-# INLINE local #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance MonadError e m => MonadError e (LevelsT m) where
   throwError = lift . throwError
   {-# INLINE throwError #-}
@@ -132,7 +132,7 @@ instance MonadError e m => MonadError e (LevelsT m) where
     catchError (f cons nil) (\e -> runLevelsT (g e) cons nil)
   {-# INLINE catchError #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance MonadIO m => MonadIO (LevelsT m) where
   liftIO m = LevelsT \cons nil -> liftIO m >>= (`cons` nil) . Bag.singleton
   {-# INLINE liftIO #-}
diff --git a/src/Control/Monad/Ref.hs b/src/Control/Monad/Ref.hs
index 670e490..b87a51c 100644
--- a/src/Control/Monad/Ref.hs
+++ b/src/Control/Monad/Ref.hs
@@ -1,6 +1,6 @@
 -- | State implemented over 'IORef'.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Control.Monad.Ref
   ( -- * RefM Transformer
     RefM (RefM),
@@ -23,7 +23,7 @@ import Data.IORef (IORef, newIORef, readIORef, writeIORef)
 -- In situations where the state @s@ is a large structure which undergoes frequent alteration, 'RefM' can be used as a
 -- more preformant alternative to state (assuming its impurity is not a concern).
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 newtype RefM s m a = RefM
   {unRefM :: IORef s -> m a}
   deriving (Functor)
@@ -38,7 +38,7 @@ runRefM (RefM k) st = do
 execRefM :: MonadIO m => RefM s m a -> s -> m s
 execRefM refM st = fst <$> runRefM refM st
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Applicative m => Applicative (RefM s m) where
   pure x = RefM \_ -> pure x
   {-# INLINE pure #-}
@@ -47,18 +47,18 @@ instance Applicative m => Applicative (RefM s m) where
     f ref <*> m ref
   {-# INLINE (<*>) #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Monad m => Monad (RefM s m) where
   RefM f >>= m = RefM \ref ->
     f ref >>= \x -> unRefM (m x) ref
   {-# INLINE (>>=) #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance MonadIO m => MonadIO (RefM s m) where
   liftIO m = RefM \_ -> liftIO m
   {-# INLINE liftIO #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance MonadIO m => MonadState s (RefM s m) where
   get = RefM (liftIO . readIORef)
   {-# INLINE get #-}
diff --git a/src/Data/World.hs b/src/Data/World.hs
index 59c561d..17100cc 100644
--- a/src/Data/World.hs
+++ b/src/Data/World.hs
@@ -31,54 +31,54 @@ import Data.Type.Rec (HasDict, Rec, ppRecListed)
 -- | The 'World' data type is a 'Rec', which is used to represent the concrete values of a model's state, paired with
 -- it's 'Fingerprint' which has much faster preformance charateristics for comparison.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data World ctx = World
   { _worldFingerprint :: {-# UNPACK #-} !Fingerprint
   , _worldValues :: Rec ctx
   }
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Eq (World ctx) where
   World fp1 _ == World fp2 _ = fp1 == fp2
   {-# INLINE (==) #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Ord (World ctx) where
   World fp1 _ `compare` World fp2 _ = fp1 `compare` fp2
   {-# INLINE compare #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Show (Rec ctx) => Show (World ctx) where
   show (World fp w) = "<<" ++ show fp ++ ":" ++ show w ++ ">>"
   {-# INLINE show #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Hashable (World ctx) where
   hashWithSalt salt (World (Fingerprint fp) _) = hashWithSalt salt fp
   {-# INLINE hashWithSalt #-}
 
 -- | Constructs a 'World' type from the given 'Rec'.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 makeWorld :: Hashable (Rec ctx) => Rec ctx -> World ctx
 makeWorld w = World (fingerprintRec w) w
 
 -- | Lens focusing on a 'World's fingerprint.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 fingerprint :: Lens' (World ctx) Fingerprint
 fingerprint = lens _worldFingerprint \World {..} x -> World {_worldFingerprint = x, ..}
 
 -- | Lens focusing on the 'Rec' holding the concrete values of a 'World'.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 worldValues :: SimpleGetter (World ctx) (Rec ctx)
 worldValues = to _worldValues
 
 -- | @'ppWorldListed' world@ lays out a list of documents for each state variable in @world@ using the world fingerprint
 -- as a header.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 ppWorldListed :: HasDict Show ctx => World ctx -> [Doc AnsiStyle]
 ppWorldListed (World hash values) =
   let hashDoc = annotate (colorDull Yellow) (pretty hash)
diff --git a/src/Language/Spectacle/AST/Action.hs b/src/Language/Spectacle/AST/Action.hs
index 2fe188f..068ab76 100644
--- a/src/Language/Spectacle/AST/Action.hs
+++ b/src/Language/Spectacle/AST/Action.hs
@@ -81,7 +81,7 @@ type ActionSyntax =
 -- | Completely evaluate a temporal action yielding either a 'RuntimeException' or a collection of new worlds accessible
 -- by the action given.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 runExceptionalAction ::
   forall ctxt.
   Hashable (Rec ctxt) =>
@@ -142,7 +142,7 @@ runAction knowns action =
 
 -- | Traverses the effects in an action, rewriting all logical operators and quantifiers scoped within a negation.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 rewriteLogic :: Members '[Logic, Quantifier, NonDet] effs => Lang ctx effs Bool -> Lang ctx effs Bool
 rewriteLogic = \case
   Pure x -> pure x
@@ -159,7 +159,7 @@ rewriteLogic = \case
 -- | Reduces logical negation by applying the usual rewrite rules to quantifiers and other logical operators scoped
 -- within the negation.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 applyComplement :: Members '[Logic, Quantifier, NonDet] effs => Lang ctx effs Bool -> Lang ctx effs Bool
 applyComplement = \case
   Pure x -> pure x
@@ -189,7 +189,7 @@ applyComplement = \case
 
 -- | Introduces the variable environment to an 'Action' "underneath" the 'Closure' effect.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 introduceEnv ::
   Lang ctx (Logic ': Closure ': Quantifier ': effs) a ->
   Lang ctx (Logic ': Closure ': Quantifier ': Env ': effs) a
diff --git a/src/Language/Spectacle/AST/Temporal.hs b/src/Language/Spectacle/AST/Temporal.hs
index f8b4c5c..a905840 100644
--- a/src/Language/Spectacle/AST/Temporal.hs
+++ b/src/Language/Spectacle/AST/Temporal.hs
@@ -1,6 +1,6 @@
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.AST.Temporal
   ( -- * Temporal Formula Monad
     Temporal,
diff --git a/src/Language/Spectacle/Exception/RuntimeException.hs b/src/Language/Spectacle/Exception/RuntimeException.hs
index b573d5e..c58570e 100644
--- a/src/Language/Spectacle/Exception/RuntimeException.hs
+++ b/src/Language/Spectacle/Exception/RuntimeException.hs
@@ -42,7 +42,7 @@ data QuantifierException where
   --
   -- would throw 'ForallViolated' since 2 is not 'odd'.
   --
-  -- @since 0.1.0.0
+  -- @since 1.0.0
   ForallViolated ::
     QuantifierException
   -- | 'ExistsViolated' is thrown when an existentially quantified set has no values that satisfy its predicate,
@@ -55,7 +55,7 @@ data QuantifierException where
   --
   -- would throw 'ExistsViolated' since there is no number @n in {2, 4}@ such that @'odd' n ≡ 'True'@
   --
-  -- @since 0.1.0.0
+  -- @since 1.0.0
   ExistsViolated ::
     QuantifierException
   deriving stock (Show, Typeable)
diff --git a/src/Language/Spectacle/Fairness.hs b/src/Language/Spectacle/Fairness.hs
index 0a3096e..4a23835 100644
--- a/src/Language/Spectacle/Fairness.hs
+++ b/src/Language/Spectacle/Fairness.hs
@@ -3,7 +3,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Fairness
   ( -- * Fairness
     Fairness (Unfair, WeakFair, StrongFair),
@@ -20,7 +20,7 @@ import Type.Reflection (Typeable, someTypeRep)
 
 -- | Enumerated fairness constraints.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data Fairness
   = Unfair
   | WeakFair
@@ -29,7 +29,7 @@ data Fairness
 
 -- | Reifies a promoted 'Fairness' constructor.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 reifyFairness :: forall (x :: Fairness). Typeable x => Fairness
 reifyFairness
   | actualTyCon == strongTyCon = StrongFair
diff --git a/src/Language/Spectacle/Interaction.hs b/src/Language/Spectacle/Interaction.hs
index 06b508d..55900fa 100644
--- a/src/Language/Spectacle/Interaction.hs
+++ b/src/Language/Spectacle/Interaction.hs
@@ -3,7 +3,7 @@
 
 -- | CLI interaction.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Interaction
   ( -- * CLI
     interaction,
diff --git a/src/Language/Spectacle/Interaction/Args.hs b/src/Language/Spectacle/Interaction/Args.hs
index 2486840..bd2346a 100644
--- a/src/Language/Spectacle/Interaction/Args.hs
+++ b/src/Language/Spectacle/Interaction/Args.hs
@@ -2,7 +2,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Interaction.Args where
 
 import Control.Applicative (liftA2)
@@ -70,7 +70,7 @@ tokenReplayOpts = between (single "+replay") (single "-replay") do
 -- 'parseSubtreeOpts' "-from 0x01234567 -to 0x01234567"
 -- @
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 parseSubtreeOpts :: ParseCLI (Fingerprint, Fingerprint)
 parseSubtreeOpts = liftA2 (,) (tokenVarArg "from" tokenFingerprint) (tokenVarArg "to" tokenFingerprint)
 
@@ -80,7 +80,7 @@ parseSubtreeOpts = liftA2 (,) (tokenVarArg "from" tokenFingerprint) (tokenVarArg
 -- 'parseDepthOpts' "-from 10 -to 12"
 -- @
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 parseDepthOpts :: ParseCLI (Int, Int)
 parseDepthOpts = liftA2 (,) (tokenVarArg "from" tokenDepth) (tokenVarArg "to" tokenDepth)
 
@@ -90,7 +90,7 @@ parseDepthOpts = liftA2 (,) (tokenVarArg "from" tokenDepth) (tokenVarArg "to" to
 -- 'parseDepthOpts' "-bound 5"
 -- @
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 parseBoundOpts :: ParseCLI Int
 parseBoundOpts = tokenVarArg "bound" tokenDepth
 
@@ -99,7 +99,7 @@ tokenDepth = read <$> inclusion (many digitChar)
 
 -- | Parse a CLI variable, which for @'tokenVarArg' "from" p@ is a string of the form "-from p(...)".
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 tokenVarArg :: String -> ParseCLI a -> ParseCLI a
 tokenVarArg varName rhs = prefixVar *> rhs
   where
diff --git a/src/Language/Spectacle/Interaction/CLI.hs b/src/Language/Spectacle/Interaction/CLI.hs
index 085de55..1ca1bec 100644
--- a/src/Language/Spectacle/Interaction/CLI.hs
+++ b/src/Language/Spectacle/Interaction/CLI.hs
@@ -3,7 +3,7 @@
 -- | This module exports the 'CLI' monad, an abstraction over command-line interactions such as emitting logs and
 -- messages from the model checker per options declared by a user.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Interaction.CLI
   ( -- * The CLI Monad
     CLI (CLI),
@@ -42,7 +42,7 @@ import qualified Language.Spectacle.Interaction.Options as Opts
 
 -- | The 'CLI' monad is a @'ReaderT' 'IO'@ carrying context of command-line options.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 newtype CLI a = CLI
   {unCLI :: ReaderT ContextCLI IO a}
   deriving stock (Functor)
@@ -52,7 +52,7 @@ newtype CLI a = CLI
 
 -- | Lower 'CLI' into 'IO' given command-line options.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 runCLI :: CLI a -> OptsCLI -> IO a
 runCLI cli opts = do
   ctx <- newContextCLI opts
@@ -69,7 +69,7 @@ runCLI cli opts = do
 
 -- | @'cliPutDoc' doc@ emits the given @doc@ using CLI context's buffer handle.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 cliPutDoc :: Doc AnsiStyle -> CLI ()
 cliPutDoc doc = do
   handle <- asks ctxHandle
@@ -89,7 +89,7 @@ cliPutDoc doc = do
 -- * The type of run the model checker took (either "model check" or "trace").
 -- * The result of the run (either "success" or "failure")
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 cliResultDoc :: Bool -> CLI (Doc AnsiStyle)
 cliResultDoc succeeded = do
   runType <- asks (mkRunTypeDoc . ctxOpts)
@@ -109,7 +109,7 @@ cliResultDoc succeeded = do
 --
 -- Note: the preferred method of construction for 'ContextCLI' is via 'newContextCLI'.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data ContextCLI = ContextCLI
   { ctxOpts :: OptsCLI
   , ctxHandle :: Handle
@@ -118,7 +118,7 @@ data ContextCLI = ContextCLI
 
 -- | Constructs a 'ContextCLI' from a set of command-line options 'OptsCLI'.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 newContextCLI :: OptsCLI -> IO ContextCLI
 newContextCLI opts = ContextCLI opts <$> Opts.handleFrom (optsLogOutput opts)
 {-# INLINE newContextCLI #-}
diff --git a/src/Language/Spectacle/Interaction/Diagram.hs b/src/Language/Spectacle/Interaction/Diagram.hs
index 22fe8dd..2d55163 100644
--- a/src/Language/Spectacle/Interaction/Diagram.hs
+++ b/src/Language/Spectacle/Interaction/Diagram.hs
@@ -52,7 +52,7 @@ data LogNode = LogNode
 
 -- | @'traverseRowsOf' f ps@ is a traversal of @f@ on rows of @ps@, collecting the results in a list.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 traverseRowsOf :: (Set Point -> DiagramM a) -> Set Point -> DiagramM [a]
 traverseRowsOf f ps =
   case takeMinRow ps of
@@ -90,7 +90,7 @@ pointSection ps = do
 -- | * | 0x8f46a202
 -- @
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 labelSection :: Tape Point -> DiagramM (Doc AnsiStyle)
 labelSection ps = do
   paths <- labelPaths ps
@@ -104,7 +104,7 @@ labelSection ps = do
 -- | | |   #field2 = 12345
 -- @
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 fieldSection :: Tape Point -> DiagramM [Doc AnsiStyle]
 fieldSection points = do
   paths <- fieldPaths points
@@ -176,13 +176,13 @@ curveSegment points lcol ucol
 -- | @'labelPaths' points@ inserts a line segment for each point in @points@, and a asterrisk for the point under
 -- focus.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 labelPaths :: Tape Point -> DiagramM (Doc AnsiStyle)
 labelPaths = iteratePaths (const (pure "* "))
 
 -- | @'labelPaths' points@ inserts a line segment for each point in @points@.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 fieldPaths :: Tape Point -> DiagramM (Doc AnsiStyle)
 fieldPaths = iteratePaths foci
   where
@@ -232,7 +232,7 @@ iterateLine handleLT handleEQ handleGT points = do
 
 -- | @'verticalSegment' len@ fills a line of length @len@ comprised of segments "│ ".
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 verticalSegment :: Int -> Doc AnsiStyle
 verticalSegment len
   | len <= 0 = Doc.tab
@@ -265,7 +265,7 @@ rightTurnSegment len
 
 -- | @'leavesPaths' len@ fills a line of length @len@ comprised of segments "┴─".
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 leavesSegment :: Int -> Doc AnsiStyle
 leavesSegment len
   | len <= 0 = mempty
@@ -332,7 +332,7 @@ getColorCtx (ColorCtx i) =
     _ -> Magenta
 {-# INLINE getColorCtx #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Semigroup ColorCtx where
   -- Note: We use addition in Z mod 6 as the semigroup for 'ColorCtx' since the 'Enum' instance is cycles through 6
   -- colors.
@@ -340,12 +340,12 @@ instance Semigroup ColorCtx where
   ColorCtx x <> ColorCtx y = ColorCtx (mod (x + y) 6)
   {-# INLINE (<>) #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Monoid ColorCtx where
   mempty = ColorCtx 0
   {-# INLINE mempty #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Enum ColorCtx where
   -- Note: AnsiStyle have six unique colors that are not black or white (cyan, red, green, yellow, blue and magenta).
   -- 'DiagramM' uses this 'Enum' instance and 'succ' to cycle through these six colors since the 'Color' datatype
diff --git a/src/Language/Spectacle/Interaction/Doc.hs b/src/Language/Spectacle/Interaction/Doc.hs
index c2258fb..d943876 100644
--- a/src/Language/Spectacle/Interaction/Doc.hs
+++ b/src/Language/Spectacle/Interaction/Doc.hs
@@ -3,7 +3,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Interaction.Doc
   ( -- * Direction
     Cardinal (CUp, CDown, CLeft, CRight),
@@ -53,13 +53,13 @@ data Cardinal
 
 -- | Concat a foldable collection with a seperator interspersed.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 sepBy :: Foldable t => Doc ann -> t (Doc ann) -> Doc ann
 sepBy s = Doc.concatWith (Doc.surround s)
 
 -- | Like 'copies', but intersperses space between each copy.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 hcopies :: Int -> Doc ann -> Doc ann
 hcopies len doc
   | len <= 0 = Doc.Internal.Empty
@@ -67,7 +67,7 @@ hcopies len doc
 
 -- | @'copies' n doc@ is a more optimal combinator for @Doc.sep . replicate n doc@
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 copies :: Int -> Doc ann -> Doc ann
 copies len doc
   | len <= 0 = Doc.Internal.Empty
@@ -75,19 +75,19 @@ copies len doc
 
 -- | @'tab'@ inserts a two-space tab.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 tab :: Doc ann
 tab = Doc.Internal.Text 2 "  "
 
 -- | @'tabs' n@ inserts n-many tabs.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 tabs :: Int -> Doc ann
 tabs len = spaces (2 * len)
 
 -- | @'spaces' n@ inserts n-many spaces.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 spaces :: Int -> Doc ann
 spaces len
   | len <= 0 = Doc.Internal.Empty
@@ -96,19 +96,19 @@ spaces len
 
 -- | @'marginr' x n@ inserts @x@ and n-many spaces after.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 marginr :: Int -> Doc ann -> Doc ann
 marginr len doc = Doc.fuse Deep (doc <> spaces len)
 
 -- | @'marginr' x n@ inserts @x@ and n-many spaces after.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 marginl :: Int -> Doc ann -> Doc ann
 marginl len doc = Doc.fuse Deep (spaces len <> doc)
 
 -- | @'segment' n a b@ is a line segment of length @n@ with @a@, @b@ the left and right endpoints.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 segment :: Int -> Doc ann -> Doc ann -> Doc ann
 segment len endl endr
   | len == 0 = Doc.Internal.Empty
@@ -117,7 +117,7 @@ segment len endl endr
 
 -- | Like 'segment', but with an extra argument to specify a 'Doc' used for the line segment.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 segmentWith :: Int -> Doc ann -> Doc ann -> Doc ann -> Doc ann
 segmentWith len doc endl endr
   | len <= 2 = endl <> endr
@@ -125,7 +125,7 @@ segmentWith len doc endl endr
 
 -- | @'spaces' n@ inserts horizontal ruler of length n.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 hruler :: Int -> Doc ann
 hruler len
   | len <= 0 = Doc.Internal.Empty
diff --git a/src/Language/Spectacle/Interaction/Options.hs b/src/Language/Spectacle/Interaction/Options.hs
index 3a180ce..679124b 100644
--- a/src/Language/Spectacle/Interaction/Options.hs
+++ b/src/Language/Spectacle/Interaction/Options.hs
@@ -1,6 +1,6 @@
 -- | Command-line interface options.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Interaction.Options
   ( -- * CLI Options
     OptsCLI (OptsCLI),
@@ -49,7 +49,7 @@ import System.IO (BufferMode (LineBuffering), Handle, IOMode (ReadWriteMode), hS
 
 -- | 'OptsCLI' is a record command-line options for configuring the model checker.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data OptsCLI = OptsCLI
   { -- | Should the state diagram be drawn?
     optsLogGraph :: Bool
@@ -62,7 +62,7 @@ data OptsCLI = OptsCLI
 
 -- | 'execOptsCLI' runs the command-line options parser.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 execOptsCLI :: IO OptsCLI
 execOptsCLI =
   let option = info (parseOptsCLI <**> helper) idm
@@ -71,7 +71,7 @@ execOptsCLI =
 
 -- | 'parseOptsCLI' is the parses command-line options into an 'OptsCLI'.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 parseOptsCLI :: Parser OptsCLI
 parseOptsCLI =
   OptsCLI
@@ -83,7 +83,7 @@ parseOptsCLI =
 
 -- | CLI parser that consumes the "only-trace" flag.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 pOnlyTrace :: Parser Bool
 pOnlyTrace =
   switch
@@ -96,7 +96,7 @@ pOnlyTrace =
 
 -- | CLI parser that consumes the "log" flag.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 pLogGraph :: Parser Bool
 pLogGraph =
   switch
@@ -112,7 +112,7 @@ pLogGraph =
 -- * @'OutputPath' str@ is a filepath to write logs to.
 -- * 'OutputStdout' represents stdout as the chosen output location.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data OutputOpt
   = OptStdout
   | OptPath FilePath
@@ -120,13 +120,13 @@ data OutputOpt
 
 -- | Is the output buffer stdout?
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 isStdout :: OutputOpt -> Bool
 isStdout opt = opt == OptStdout
 
 -- | @'handleFrom' opt@ will extract the file hand from the given 'OutputOpt' @opt@.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 handleFrom :: OutputOpt -> IO Handle
 handleFrom opt = do
   handle <- case opt of
@@ -139,13 +139,13 @@ handleFrom opt = do
 -- | CLI parser that consumes the result of 'pOutputPath' if an output path is provided, otherwise 'OutputStd' is
 -- returned by default and logs will be written to stdout.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 pOutputOpt :: Parser OutputOpt
 pOutputOpt = pOutputPath <|> pure OptStdout
 
 -- | CLI parser that consumes a filepath to emit logs to.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 pOutputPath :: Parser OutputOpt
 pOutputPath = OptPath <$> parser
   where
diff --git a/src/Language/Spectacle/Interaction/Paths.hs b/src/Language/Spectacle/Interaction/Paths.hs
index 907165c..015ff13 100644
--- a/src/Language/Spectacle/Interaction/Paths.hs
+++ b/src/Language/Spectacle/Interaction/Paths.hs
@@ -2,7 +2,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Interaction.Paths
   ( -- * Construction
     toPointSet,
@@ -50,7 +50,7 @@ toPointSet = flip execState Set.empty . start
 
 -- | Like 'splitRow', but always splits on the least row in the set.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 takeMinRow :: Set Point -> (Set Point, Set Point)
 takeMinRow ps =
   case Set.minView ps of
@@ -60,7 +60,7 @@ takeMinRow ps =
 -- | @'splitRow' i ps@ returns a subset of @ps@ containing all elements located on row @i@ and a new set stripped of
 -- this row.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 splitRow :: Int -> Set Point -> (Set Point, Set Point)
 splitRow i = seek Set.empty
   where
diff --git a/src/Language/Spectacle/Interaction/Point.hs b/src/Language/Spectacle/Interaction/Point.hs
index 8c79939..1cdda4c 100644
--- a/src/Language/Spectacle/Interaction/Point.hs
+++ b/src/Language/Spectacle/Interaction/Point.hs
@@ -4,7 +4,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Interaction.Point
   ( -- * Points
     Point (Point),
@@ -57,7 +57,7 @@ fromWorld (World hash fs0) = Point hash (docFields fs0) Nothing 0 (Pos 0 0)
         ConE n x xs -> pretty n <+> "=" <+> viaShow x : docFields xs
         NilE -> []
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Eq Point where
   pt0 == pt1 =
     let lblEq = pt0 ^. label == pt1 ^. label
@@ -65,7 +65,7 @@ instance Eq Point where
      in lblEq && posEq
   {-# INLINE (==) #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Ord Point where
   compare x y = case (compare `on` pointPos) x y of
     EQ -> (compare `on` pointLabel) x y
diff --git a/src/Language/Spectacle/Interaction/Pos.hs b/src/Language/Spectacle/Interaction/Pos.hs
index a72a9d7..57d0852 100644
--- a/src/Language/Spectacle/Interaction/Pos.hs
+++ b/src/Language/Spectacle/Interaction/Pos.hs
@@ -43,7 +43,7 @@
 -- fromList [(0,4), (1,3), (1,4), (1,5), (2,3), (2,4), (2,5), ..., (5,4), (6,4)]
 -- @
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Interaction.Pos
   ( -- * Locations
     Loc (Loc),
@@ -72,20 +72,20 @@ import Lens.Micro.Extras (view)
 
 -- | A 'Loc' is a position annotated with an length/span.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data Loc = Loc
   { locPos :: {-# UNPACK #-} !Pos
   , locExt :: {-# UNPACK #-} !Int
   }
   deriving (Eq)
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Ord Loc where
   compare = compare `on` locPos
 
 -- | Buffer row/column positions.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 newtype Pos = MkPos {getPos :: (Int, Int)}
   deriving (Eq, Semigroup, Monoid) via (Sum Int, Sum Int)
 
@@ -94,7 +94,7 @@ pattern Pos {posRow, posCol} = MkPos (posRow, posCol)
 
 {-# COMPLETE Pos #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Ord Pos where
   -- The derived implementation of 'Ord' is equivalent to what is given here, but its defined explicitly anyway
   -- to emphasize the row value superseding the order of the column value in this trichotomy.
@@ -102,7 +102,7 @@ instance Ord Pos where
     EQ -> compare y v
     ordering -> ordering
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Show Pos where
   show (Pos r c) = "Pos(" ++ show r ++ ":" ++ show c ++ ")"
 
diff --git a/src/Language/Spectacle/Lang.hs b/src/Language/Spectacle/Lang.hs
index 152a68e..7f85a09 100644
--- a/src/Language/Spectacle/Lang.hs
+++ b/src/Language/Spectacle/Lang.hs
@@ -5,7 +5,7 @@
 
 -- | The 'Lang' monad and functions for defining Spectacles syntax as effects.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Lang
   ( -- * Lang
     Lang (Pure, Op, Scoped),
@@ -52,7 +52,7 @@ import Language.Spectacle.Lang.Scoped
 
 -- | Used to unwrap the pure value in 'Lang' after all of its effects have been discharged.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 runLang :: Lang ctx '[] a -> a
 runLang (Pure x) = x
 runLang _ =
@@ -75,7 +75,7 @@ runLang _ =
 -- | Appends an effect label @eff@ to the head of a 'Lang's effect signature by the weakening rule
 -- for sum types.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 weaken :: forall eff effs ctx a. Lang ctx effs a -> Lang ctx (eff ': effs) a
 weaken = \case
   Pure x -> pure x
diff --git a/src/Language/Spectacle/Lang/Internal.hs b/src/Language/Spectacle/Lang/Internal.hs
index f80c53f..905367c 100644
--- a/src/Language/Spectacle/Lang/Internal.hs
+++ b/src/Language/Spectacle/Lang/Internal.hs
@@ -2,7 +2,7 @@
 
 -- | The 'Lang' monad.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Lang.Internal
   ( Lang (Pure, Op, Scoped),
     send,
@@ -35,7 +35,7 @@ import Language.Spectacle.Syntax.NonDet.Internal (NonDet (Choose, Empty))
 --
 -- * The type parameter @effs@ is the set of effects a 'Lang' is capable of performing.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 type Lang :: [Ascribe Symbol Type] -> [EffectK] -> Type -> Type
 data Lang ctxt effs a where
   Pure ::
@@ -52,26 +52,26 @@ data Lang ctxt effs a where
 
 -- | Sends a constructor for the effect @eff@ for 'Lang' to handle.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 send :: Member eff effs => eff a -> Lang ctx effs a
 send eff = Op (inject eff) pure
 {-# INLINE send #-}
 
 -- | Like 'send', but sends a constructor for the 'Effect' instance of @eff@.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 scope :: Member eff effs => Effect eff (Lang ctx effs) a -> Lang ctx effs a
 scope eff = Scoped (injectS eff) Loom.identity
 {-# INLINE scope #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Functor (Lang ctx effs) where
   fmap f (Pure x) = Pure (f x)
   fmap f (Op u k) = Op u (fmap f . k)
   fmap f (Scoped u loom) = Scoped u (fmap f loom)
   {-# INLINE fmap #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Applicative (Lang ctx effs) where
   pure = Pure
   {-# INLINE CONLIKE pure #-}
@@ -81,14 +81,14 @@ instance Applicative (Lang ctx effs) where
   Scoped u (Loom ctx eta) <*> m = Scoped u (Loom ctx ((<*> m) . eta))
   {-# INLINE (<*>) #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Monad (Lang ctx effs) where
   Pure x >>= f = f x
   Op u k >>= f = Op u (k >=> f)
   Scoped u loom >>= f = Scoped u (loom ~>~ bind f)
   {-# INLINE (>>=) #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Member NonDet effs => Alternative (Lang ctx effs) where
   empty = send Empty
   {-# INLINE empty #-}
@@ -96,7 +96,7 @@ instance Member NonDet effs => Alternative (Lang ctx effs) where
   a <|> b = send Choose >>= bool b a
   {-# INLINE (<|>) #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Member NonDet effs => MonadPlus (Lang ctx effs) where
   mzero = empty
   {-# INLINE mzero #-}
diff --git a/src/Language/Spectacle/Lang/Member.hs b/src/Language/Spectacle/Lang/Member.hs
index 8b80863..b9f41f5 100644
--- a/src/Language/Spectacle/Lang/Member.hs
+++ b/src/Language/Spectacle/Lang/Member.hs
@@ -2,7 +2,7 @@
 
 -- | Effect membership.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Lang.Member
   ( Members,
     Member (inject, project, injectS, projectS),
@@ -21,7 +21,7 @@ import Language.Spectacle.Lang.Scoped (Effect, EffectK, Scoped (SHere, SThere))
 -- * @Members '[A, B, C] effs = (Member A effs, Member B effs, Member C effs)@
 -- * @Members A effs = Members '[A] effs = Member A effs@
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 type Members :: forall k. k -> [EffectK] -> Constraint
 type family Members eff effs where
 -- Type ascription is used here rather than a type application to the LHS of the equations since
@@ -34,31 +34,31 @@ type family Members eff effs where
 
 -- | An effect @eff@ is a member of the effect signature @effs@ if @eff@ occurs in @effs@.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 type Member :: EffectK -> [EffectK] -> Constraint
 class Member eff effs where
   -- | Inject a first order effect @eff a@ into a sum of first-order effects 'Op'. Higher-order
   -- operations must be injected with 'injectS'.
   --
-  -- @since 0.1.0.0
+  -- @since 1.0.0
   inject :: eff a -> Op effs a
 
   -- | Projects the effect @eff@ from the given 'Op' if it is the inhabitant, otherwise 'Nothing'.
   --
-  -- @since 0.1.0.0
+  -- @since 1.0.0
   project :: Op effs a -> Maybe (eff a)
 
   -- | Like 'inject', but specifically for scoped operations.
   --
-  -- @since 0.1.0.0
+  -- @since 1.0.0
   injectS :: Effect eff m a -> Scoped effs m a
 
   -- | Like 'project', but specifically for scoped operations.
   --
-  -- @since 0.1.0.0
+  -- @since 1.0.0
   projectS :: Scoped effs m a -> Maybe (Effect eff m a)
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance {-# OVERLAPS #-} Member eff (eff ': effs) where
   inject = OHere
   {-# INLINE CONLIKE inject #-}
@@ -79,7 +79,7 @@ instance {-# OVERLAPS #-} Member eff (eff ': effs) where
   projectS (SThere _) = Nothing
   {-# INLINE CONLIKE projectS #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Member eff effs => Member eff (eff' ': effs) where
   inject = OThere . inject
   {-# INLINE CONLIKE inject #-}
diff --git a/src/Language/Spectacle/Lang/Op.hs b/src/Language/Spectacle/Lang/Op.hs
index 71447f2..dfc4435 100644
--- a/src/Language/Spectacle/Lang/Op.hs
+++ b/src/Language/Spectacle/Lang/Op.hs
@@ -2,7 +2,7 @@
 
 -- | First-order effect operations.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Lang.Op
   ( Op (OHere, OThere),
     decomposeOp,
@@ -14,7 +14,7 @@ where
 
 -- | 'Op' is an extensible sum inhabited by a first-order effect @eff a@ in @effs@.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data Op effs a where
   OHere :: eff a -> Op (eff ': effs) a
   OThere :: Op effs a -> Op (eff ': effs) a
@@ -22,7 +22,7 @@ data Op effs a where
 -- | Orthogonal decomposition for 'Op'. Yields either a proof that the effect @eff@ is not
 -- inhabiting the given 'Op' or a constructor for @eff@.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 decomposeOp :: Op (eff ': effs) a -> Either (Op effs a) (eff a)
 decomposeOp (OHere eff) = Right eff
 decomposeOp (OThere op) = Left op
@@ -30,7 +30,7 @@ decomposeOp (OThere op) = Left op
 
 -- | A special case of 'decomposeOp'. A singleton sum of @eff@ must be inhabited by @eff@.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 extractOp :: Op '[eff] a -> eff a
 extractOp (OHere eff) = eff
 extractOp (OThere op) = case op of
diff --git a/src/Language/Spectacle/Lang/Scoped.hs b/src/Language/Spectacle/Lang/Scoped.hs
index 17c5d01..6747e80 100644
--- a/src/Language/Spectacle/Lang/Scoped.hs
+++ b/src/Language/Spectacle/Lang/Scoped.hs
@@ -66,7 +66,7 @@
 -- 1. [Effect Handlers in Haskell, Evidently](https://xnning.github.io/papers/haskell-evidently.pdf)
 -- 2. [Effect Handlers in Scope](https://www.cs.ox.ac.uk/people/nicolas.wu/papers/Scope.pdf)
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Lang.Scoped
   ( -- * Effect Kinds
     EffectK,
@@ -91,24 +91,24 @@ import Data.Void (Void)
 
 -- | The kind of first-order effects.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 type EffectK = Type -> Type
 
 -- | The kind of higher-order effects.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 type ScopeK = (Type -> Type) -> Type -> Type
 
 -- | Constraint for first-order effects.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 type FirstOrder :: EffectK -> Constraint
 
 type FirstOrder eff = forall m a. Coercible (Effect eff m a) Void
 
 -- | 'Effect' is a family of higher-order operations for the effect @eff@.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 type Effect :: EffectK -> ScopeK
 data family Effect eff m a
 
@@ -117,7 +117,7 @@ data family Effect eff m a
 -- | 'Scoped' is an extensible sum inhabited by the higher-order operations of some effect in
 -- @effs@.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data Scoped effs m a where
   SHere :: Effect eff m a -> Scoped (eff ': effs) m a
   SThere :: Scoped effs m a -> Scoped (eff ': effs) m a
@@ -126,7 +126,7 @@ data Scoped effs m a where
 -- instance for @eff@ or witness a proof that @Eff eff m a@ does not inhabit this sum and remove
 -- it from the effect signature.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 decomposeS :: Scoped (eff ': effs) m a -> Either (Scoped effs m a) (Effect eff m a)
 decomposeS (SHere eff) = Right eff
 decomposeS (SThere s) = Left s
@@ -134,7 +134,7 @@ decomposeS (SThere s) = Left s
 
 -- | A special case of 'decomposeS'. A singleton sum of @eff@ must be inhabited by @eff@.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 extractS :: Scoped '[eff] m a -> Effect eff m a
 extractS (SHere eff) = eff
 extractS (SThere s) = case s of
diff --git a/src/Language/Spectacle/Model.hs b/src/Language/Spectacle/Model.hs
index 9ca0b06..cb27cdf 100644
--- a/src/Language/Spectacle/Model.hs
+++ b/src/Language/Spectacle/Model.hs
@@ -1,6 +1,6 @@
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Model where
 
 import Control.Monad (unless)
@@ -283,7 +283,7 @@ unfoldModelState actions = traverse go . Set.toList
 
 -- | 'throwRefute' is a helper combination for constructing an error refuting a temporal property and throwing it.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 throwRefute :: Monad m => Modality -> String -> Maybe (World ctx) -> Maybe (World ctx) -> ModelM ctx m a
 throwRefute modality name here there = do
   let err = TemporalError modality name here there
@@ -291,24 +291,24 @@ throwRefute modality name here there = do
 
 -- | Convinence function for constructing an "always" error and throwing it.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 throwRefuteAlways :: Monad m => String -> Maybe (World ctx) -> Maybe (World ctx) -> ModelM ctx m a
 throwRefuteAlways = throwRefute Always
 
 -- | Convinence function for constructing an "eventually" error and throwing it.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 throwRefuteEventually :: Monad m => String -> Maybe (World ctx) -> Maybe (World ctx) -> ModelM ctx m a
 throwRefuteEventually = throwRefute Eventually
 
 -- | Convinence function for constructing an "infinitely often" error and throwing it.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 throwRefuteInfinitely :: Monad m => String -> Maybe (World ctx) -> Maybe (World ctx) -> ModelM ctx m a
 throwRefuteInfinitely = throwRefute Infinitely
 
 -- | Convinence function for constructing an "stays as" error and throwing it.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 throwRefuteStays :: Monad m => String -> Maybe (World ctx) -> Maybe (World ctx) -> ModelM ctx m a
 throwRefuteStays = throwRefute Stays
diff --git a/src/Language/Spectacle/Model/ModelAction.hs b/src/Language/Spectacle/Model/ModelAction.hs
index dfad264..302a743 100644
--- a/src/Language/Spectacle/Model/ModelAction.hs
+++ b/src/Language/Spectacle/Model/ModelAction.hs
@@ -1,6 +1,6 @@
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Model.ModelAction
   ( -- * Model Action
     ModelAction (ModelAction),
diff --git a/src/Language/Spectacle/Model/ModelEnv.hs b/src/Language/Spectacle/Model/ModelEnv.hs
index 030055f..3211f08 100644
--- a/src/Language/Spectacle/Model/ModelEnv.hs
+++ b/src/Language/Spectacle/Model/ModelEnv.hs
@@ -2,7 +2,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Model.ModelEnv
   ( -- * Model Environments
     ModelEnv (ModelEnv),
diff --git a/src/Language/Spectacle/Model/ModelError.hs b/src/Language/Spectacle/Model/ModelError.hs
index 727cb2f..92742d5 100644
--- a/src/Language/Spectacle/Model/ModelError.hs
+++ b/src/Language/Spectacle/Model/ModelError.hs
@@ -4,7 +4,7 @@
 
 -- | Model checker errors.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Model.ModelError
   ( -- * Model Errors
     ModelError (InitialError, RuntimeError, RefutedError),
@@ -40,7 +40,7 @@ import Language.Spectacle.Specification.Prop (Modality, ppModality)
 
 -- | 'TemporalError' captures information about a temporal property refutation.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data ModelError :: [Ascribe Symbol Type] -> Type where
   InitialError ::
     ModelError ctx
@@ -51,7 +51,7 @@ data ModelError :: [Ascribe Symbol Type] -> Type where
     TemporalError ctx ->
     ModelError ctx
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 deriving instance HasDict Show ctx => Show (ModelError ctx)
 
 ppModelError :: HasDict Show ctx => ModelError ctx -> Doc AnsiStyle
@@ -70,7 +70,7 @@ ppRuntimeError exc = "runtime error:" <+> viaShow exc
 
 -- | 'TemporalError' captures information about a temporal property refutation.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data TemporalError ctx = TemporalError
   { errorModality :: Modality
   , errorPropName :: String
@@ -78,7 +78,7 @@ data TemporalError ctx = TemporalError
   , errorPlains :: Maybe (World ctx)
   }
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 deriving instance HasDict Show ctx => Show (TemporalError ctx)
 
 ppTemporalError :: HasDict Show ctx => TemporalError ctx -> Doc AnsiStyle
diff --git a/src/Language/Spectacle/Model/ModelNode.hs b/src/Language/Spectacle/Model/ModelNode.hs
index cc3ac04..7df1a80 100644
--- a/src/Language/Spectacle/Model/ModelNode.hs
+++ b/src/Language/Spectacle/Model/ModelNode.hs
@@ -3,7 +3,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Model.ModelNode
   ( -- * Model State Nodes
     ModelNode (ModelNode),
@@ -36,13 +36,13 @@ data ModelNode ctx = ModelNode
   , nodeValuation :: Rec ctx
   }
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 deriving instance HasDict Show ctx => Show (ModelNode ctx)
 
 -- | @'nextEntries' name@ produces a list of 'Fingerprint's following the action named @name@ for the node's
 -- valuation.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 nextEntries :: String -> Lens' (ModelNode ctx) [Fingerprint]
 nextEntries name =
   let getter ModelNode {..} = nodeNextEntries Map.! name
@@ -58,24 +58,24 @@ queuedOf =
 
 -- | Is the action with given name enabled?
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 isEnabled :: String -> SimpleGetter (ModelNode ctx) Bool
 isEnabled name = nextEntries name . to (not . null)
 
 -- | Is the action with given name disabled?
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 isDisabled :: String -> SimpleGetter (ModelNode ctx) Bool
 isDisabled name = nextEntries name . to null
 
 -- | 'actionsOf' is a lens focusing on the set of actions taken at a 'ModelNode'.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 actionsOf :: SimpleGetter (ModelNode ctx) [String]
 actionsOf = to (Map.keys . nodeNextEntries)
 
 -- | 'nodeValuation' is a lens focusing on the valuation of variables this node represents.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 valuation :: SimpleGetter (ModelNode ctx) (Rec ctx)
 valuation = to nodeValuation
diff --git a/src/Language/Spectacle/Model/ModelState.hs b/src/Language/Spectacle/Model/ModelState.hs
index 17f00b7..6dca242 100644
--- a/src/Language/Spectacle/Model/ModelState.hs
+++ b/src/Language/Spectacle/Model/ModelState.hs
@@ -3,7 +3,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Model.ModelState
   ( -- * ModelState
     ModelState (ModelState),
@@ -35,7 +35,7 @@ newtype ModelState ctx = ModelState
   {getModelState :: IntMap (ModelNode ctx)}
   deriving (Semigroup, Monoid) via IntMap (ModelNode ctx)
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 deriving instance HasDict Show ctx => Show (ModelState ctx)
 
 indexNode :: Fingerprint -> Lens' (ModelState ctx) (ModelNode ctx)
diff --git a/src/Language/Spectacle/Model/ModelTemporal.hs b/src/Language/Spectacle/Model/ModelTemporal.hs
index 4062fe4..defdbdf 100644
--- a/src/Language/Spectacle/Model/ModelTemporal.hs
+++ b/src/Language/Spectacle/Model/ModelTemporal.hs
@@ -1,6 +1,6 @@
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Model.ModelTemporal
   ( -- * Model Temporal Formulae
     ModelTemporal (ModelTemporal),
diff --git a/src/Language/Spectacle/Model/Monad.hs b/src/Language/Spectacle/Model/Monad.hs
index a5e2ae9..d6a9ef2 100644
--- a/src/Language/Spectacle/Model/Monad.hs
+++ b/src/Language/Spectacle/Model/Monad.hs
@@ -2,7 +2,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Model.Monad
   ( -- * Model Monad
     ModelIO,
@@ -65,11 +65,11 @@ runModelM model env st =
     & flip runReaderT env
     & flip runRefM st
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 deriving instance MonadIO m => MonadState (ModelState ctx) (ModelM ctx m)
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 deriving instance Monad m => MonadReader ModelEnv (ModelM ctx m)
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 deriving instance Monad m => MonadError (ModelError ctx) (ModelM ctx m)
diff --git a/src/Language/Spectacle/RTS/Registers.hs b/src/Language/Spectacle/RTS/Registers.hs
index c0fd0b9..a6097d5 100644
--- a/src/Language/Spectacle/RTS/Registers.hs
+++ b/src/Language/Spectacle/RTS/Registers.hs
@@ -3,7 +3,7 @@
 
 -- | Runtime state used to implement call-by-need evaluation of closures and variable substitution.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.RTS.Registers
   ( RuntimeState (RuntimeState, plains, primes, callStack, newValues),
     emptyRuntimeState,
@@ -48,7 +48,7 @@ type StateFunSyntax = '[Prime, Plain, NonDet, Error RuntimeException]
 -- * 'callStack' tracks the substitution of primed variables which is used guard against a cyclic
 -- variable relations.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data RuntimeState ctx = RuntimeState
   { plains :: Rec ctx
   , primes :: Registers ctx
@@ -69,7 +69,7 @@ emptyRuntimeState r =
 
 -- | A record of 'Thunk's.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 newtype Registers ctxt = Registers
   {unRegisters :: RecF (Thunk ctxt) ctxt}
 
@@ -77,25 +77,25 @@ deriving instance Show (RecF (Thunk ctxt) ctxt) => Show (Registers ctxt)
 
 -- | Construct a 'Registers' of unrelated primed variables.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 emptyRegisters :: Rec ctx -> Registers ctx
 emptyRegisters = Registers . Rec.mapF \_ (Identity _) -> Unchanged
 
 -- | Retrieves the value of the variable named @s@ in 'Registers' as a 'Thunk'.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 getRegister :: Has s a ctx => Name s -> Registers ctx -> Thunk ctx a
 getRegister n (Registers rs) = Rec.getF n rs
 
 -- | Sets the value of the variable named @s@ to the result given by evaluating a 'Thunk'.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 setRegister :: Has s a ctx => Name s -> a -> Registers ctx -> Registers ctx
 setRegister n x (Registers rs) = Registers (Rec.setF n (Evaluated x) rs)
 
 -- | Sets the value of the variable named @s@ in 'Registers' to an unevaluated expression.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 setThunk :: Has s a ctx => Name s -> StateFun ctx a -> Registers ctx -> Registers ctx
 setThunk n m (Registers rs) = Registers (Rec.setF n (Thunk m) rs)
 
@@ -105,13 +105,13 @@ setThunk n m (Registers rs) = Registers (Rec.setF n (Thunk m) rs)
 -- * 'Evaluated' result of evaluating a thunk in current world.
 -- * Any primed variable is implicitly 'Unchanged' if it has not been related in the current world.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data Thunk ctxt a
   = Thunk (StateFun ctxt a)
   | Evaluated a
   | Unchanged
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Show a => Show (Thunk (s # a ': ctx) a) where
   show (Thunk _) = "<<thunk>>"
   show (Evaluated x) = show x
diff --git a/src/Language/Spectacle/Specification/Action.hs b/src/Language/Spectacle/Specification/Action.hs
index 34cdd4d..f39f44d 100644
--- a/src/Language/Spectacle/Specification/Action.hs
+++ b/src/Language/Spectacle/Specification/Action.hs
@@ -4,7 +4,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Specification.Action
   ( -- * ActionType
     ActionType (ActionUF, ActionWF, ActionSF),
@@ -26,7 +26,7 @@ import Language.Spectacle.Fairness (Fairness (StrongFair, Unfair, WeakFair), rei
 
 -- | Action declarations.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 data ActionType :: [Ascribe Symbol Type] -> Fairness -> Type where
   ActionUF :: Action ctx Bool -> ActionType ctx 'Unfair
   ActionWF :: Action ctx Bool -> ActionType ctx 'WeakFair
diff --git a/src/Language/Spectacle/Specification/Prop.hs b/src/Language/Spectacle/Specification/Prop.hs
index 2f35475..5bf4b54 100644
--- a/src/Language/Spectacle/Specification/Prop.hs
+++ b/src/Language/Spectacle/Specification/Prop.hs
@@ -3,7 +3,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Specification.Prop
   ( -- * Temporal Formula
     TemporalType (PropG, PropF, PropGF, PropFG),
diff --git a/src/Language/Spectacle/Specification/Variable.hs b/src/Language/Spectacle/Specification/Variable.hs
index 89ef366..a302d2b 100644
--- a/src/Language/Spectacle/Specification/Variable.hs
+++ b/src/Language/Spectacle/Specification/Variable.hs
@@ -4,7 +4,7 @@
 
 -- |
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Specification.Variable
   ( -- * Syntax
     Var ((:=)),
@@ -45,14 +45,14 @@ class HasVars a where
 
   runInitActions :: VarCtxt a ~ ctxt => a -> RecF (Lang '[] '[NonDet]) ctxt
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance (HasVars a, HasVars b) => HasVars (a :. b) where
   type VarCtxt (a :. b) = VarCtxt a ++ VarCtxt b
 
   runInitActions (xs :. ys) = Rec.concatF (runInitActions xs) (runInitActions ys)
   {-# INLINE runInitActions #-}
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance HasVars (Var var ty) where
   type VarCtxt (Var var ty) = (var # ty) ': '[]
 
diff --git a/src/Language/Spectacle/Syntax/Closure.hs b/src/Language/Spectacle/Syntax/Closure.hs
index 8f8ce51..dce16c2 100644
--- a/src/Language/Spectacle/Syntax/Closure.hs
+++ b/src/Language/Spectacle/Syntax/Closure.hs
@@ -1,6 +1,6 @@
 -- | Closures and variable relations.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Syntax.Closure
   ( Closure (Closure),
     Effect (Close),
@@ -53,7 +53,7 @@ import Language.Spectacle.Syntax.Prime (RuntimeState (primes), substitute)
 --     return True -- relate the value to the next frame, @return (odd n)@ could be written to exclude even n.
 -- @
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 infix 4 .=
 
 (.=) :: (Member Closure effs, Has s a ctx) => Name s -> StateFun ctx a -> Lang ctx effs ()
@@ -62,7 +62,7 @@ name .= expr = scope (Close name expr)
 
 -- | Discharges a 'Closure' effect, returning a 'Rec' new values for each variable in @ctx@.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 runActionClosure ::
   Members '[NonDet, Env, Error RuntimeException] effs =>
   Lang ctx (Closure ': effs) a ->
@@ -72,7 +72,7 @@ runActionClosure m = evaluateThunks (makeThunks m)
 
 -- | Evaluates all unevaluated closures in a specification.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 evaluateThunks ::
   Members '[NonDet, Env, Error RuntimeException] effs =>
   Lang ctx (Closure ': effs) a ->
@@ -103,7 +103,7 @@ evaluateThunks = \case
 -- by 'evaluateThunks'. An extra pass is needed to register all closures before substitution of
 -- primed variables takes place.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 makeThunks ::
   Members '[Closure, Env, Error RuntimeException] effs =>
   Lang ctx effs a ->
diff --git a/src/Language/Spectacle/Syntax/Error.hs b/src/Language/Spectacle/Syntax/Error.hs
index b9757b7..b0c9e8b 100644
--- a/src/Language/Spectacle/Syntax/Error.hs
+++ b/src/Language/Spectacle/Syntax/Error.hs
@@ -1,6 +1,6 @@
 -- | The 'Error' effect for throwing exceptions which can be caught.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Syntax.Error
   ( Error (ThrowE),
     Effect (CatchE),
@@ -27,19 +27,19 @@ import Language.Spectacle.Syntax.Error.Internal (Effect (CatchE), Error (ThrowE)
 -- | Throw an error of type @e@, escaping the current continuation up to the nearest enclosing
 -- 'catchE'.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 throwE :: Member (Error e) effs => e -> Lang ctx effs a
 throwE e = send (ThrowE e)
 
 -- | Catch an error of type @e@ continuting from the provided function if an error was thrown.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 catchE :: Member (Error e) effs => Lang ctx effs a -> (e -> Lang ctx effs a) -> Lang ctx effs a
 catchE m f = scope (CatchE m f)
 
 -- | Discharge an 'Error' effect into either an error or the result of a successful computation.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 runError :: Lang ctx (Error e ': effs) a -> Lang ctx effs (Either e a)
 runError = \case
   Pure x -> pure (Right x)
diff --git a/src/Language/Spectacle/Syntax/Logic.hs b/src/Language/Spectacle/Syntax/Logic.hs
index 96f9952..b8d91ef 100644
--- a/src/Language/Spectacle/Syntax/Logic.hs
+++ b/src/Language/Spectacle/Syntax/Logic.hs
@@ -1,6 +1,6 @@
 -- | Quantifiers and logic.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Syntax.Logic
   ( Logic (Logic),
     Effect (Complement, Conjunct, Disjunct),
@@ -36,42 +36,42 @@ import Language.Spectacle.Syntax.NonDet (NonDet)
 -- | Logical negation. The 'complement' operator is equivalent to 'not' for simple expressions, but
 -- can be used to negate quantifiers and the other logical operators in spectacle.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 complement :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool
 complement m = scope (Complement m)
 {-# INLINE complement #-}
 
 -- | Boolean conjunction.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 conjunct :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool -> Lang ctx effs Bool
 conjunct m n = scope (Conjunct m n)
 {-# INLINE conjunct #-}
 
 -- | Boolean disjunction.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 disjunct :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool -> Lang ctx effs Bool
 disjunct m n = scope (Disjunct m n)
 {-# INLINE disjunct #-}
 
 -- | Logical implication.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 implies :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool -> Lang ctx effs Bool
 implies m n = disjunct (complement m) n
 {-# INLINE implies #-}
 
 -- | If and only if.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 iff :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool -> Lang ctx effs Bool
 iff m n = conjunct (implies m n) (implies n m)
 {-# INLINE iff #-}
 
 -- | Discharge a 'Logic' effect.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 runLogic ::
   forall ctx effs.
   Members '[Error RuntimeException, NonDet] effs =>
diff --git a/src/Language/Spectacle/Syntax/NonDet.hs b/src/Language/Spectacle/Syntax/NonDet.hs
index 570287e..e802bd0 100644
--- a/src/Language/Spectacle/Syntax/NonDet.hs
+++ b/src/Language/Spectacle/Syntax/NonDet.hs
@@ -2,7 +2,7 @@
 
 -- | The 'NonDet' effect models nondeterminism.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Syntax.NonDet
   ( NonDet (Choose, Empty),
     Effect (MSplit),
@@ -32,28 +32,28 @@ import Language.Spectacle.Syntax.NonDet.Internal (Effect (MSplit), NonDet (Choos
 
 -- | Nondeterministically choose an element from a foldable container.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 oneOf :: (Foldable t, Alternative m) => t a -> m a
 oneOf = foldMapA pure
 {-# INLINE oneOf #-}
 
 -- | Like `foldMap`, but folds under 'Alternative' rather than 'Monoid'.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 foldMapA :: (Foldable t, Alternative m) => (a -> m b) -> t a -> m b
 foldMapA f = getAlt . foldMap (Alt . f)
 {-# INLINE foldMapA #-}
 
 -- | Splits a 'Lang' into its 'Alternative' branches, if it has any.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 msplit :: Member NonDet effs => Lang ctx effs a -> Lang ctx effs (Maybe (Lang ctx effs a, Lang ctx effs a))
 msplit m = scope (MSplit m)
 {-# INLINE msplit #-}
 
 -- | Discharge a 'NonDet' effect into some 'Alternative' functor @f@.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 runNonDetA :: Alternative f => Lang ctx (NonDet ': effs) a -> Lang ctx effs (f a)
 runNonDetA = \case
   Pure x -> pure (pure x)
diff --git a/src/Language/Spectacle/Syntax/Plain.hs b/src/Language/Spectacle/Syntax/Plain.hs
index 7094ee8..39e4a3a 100644
--- a/src/Language/Spectacle/Syntax/Plain.hs
+++ b/src/Language/Spectacle/Syntax/Plain.hs
@@ -1,6 +1,6 @@
 -- | Plain or known variable usage and substitution.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Syntax.Plain
   ( Plain (Plain),
     Effect (PlainVar),
@@ -22,7 +22,7 @@ import Language.Spectacle.Syntax.Plain.Internal (Effect (PlainVar), Plain (Plain
 
 -- | 'plain' for a variable named @s@ is the value of @s@ from the previous frame of time.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 plain :: (Member Plain effs, Has s a ctx) => Name s -> Lang ctx effs a
 plain nm = scope (PlainVar nm)
 {-# INLINE plain #-}
@@ -30,7 +30,7 @@ plain nm = scope (PlainVar nm)
 -- | Discharge a 'Plain' effect, substituting instances of 'PlainVar' for the values in the given
 -- 'Data.Type.Rec'.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 runPlain :: Rec ctx -> Lang ctx (Plain ': effs) a -> Lang ctx effs a
 runPlain vars = \case
   Pure x -> pure x
diff --git a/src/Language/Spectacle/Syntax/Prime.hs b/src/Language/Spectacle/Syntax/Prime.hs
index 6708d77..a059af0 100644
--- a/src/Language/Spectacle/Syntax/Prime.hs
+++ b/src/Language/Spectacle/Syntax/Prime.hs
@@ -1,6 +1,6 @@
 -- | Prime (or time) variable usage and substitution.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 module Language.Spectacle.Syntax.Prime
   ( -- * Labels
     Prime (Prime),
@@ -67,7 +67,7 @@ import Language.Spectacle.Syntax.Prime.Internal
 
 -- | 'prime' for a variable named @s@ is the value of @s@ in the next time frame.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 prime :: (Member Prime effs, Has s a ctx) => Name s -> Lang ctx effs a
 prime nm = scope (PrimeVar nm)
 {-# INLINE prime #-}
@@ -75,7 +75,7 @@ prime nm = scope (PrimeVar nm)
 -- | Discharges a 'Prime' effect. This interpreter carries out the substitution of primed variables
 -- using a call-by-need evaluation strategy.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 runPrime ::
   forall ctx effs a.
   Members '[Env, Error RuntimeException, NonDet] effs =>
@@ -110,7 +110,7 @@ runPrime = \case
 -- | Alternative interpreter for 'Prime' that substitutes with a 'Rec' rather than a record of
 -- thunks.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 substPrime :: Rec ctx -> Lang ctx (Prime ': effs) a -> Lang ctx effs a
 substPrime vars = \case
   Pure x -> pure x
@@ -126,7 +126,7 @@ substPrime vars = \case
 
 -- | Evaluates the thunk for a primed variable.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 substitute ::
   (Members '[Env, NonDet, Error RuntimeException] effs, Has s a ctx) =>
   Name s ->
diff --git a/src/Language/Spectacle/Syntax/Quantifier.hs b/src/Language/Spectacle/Syntax/Quantifier.hs
index 98c4aae..94b0ac0 100644
--- a/src/Language/Spectacle/Syntax/Quantifier.hs
+++ b/src/Language/Spectacle/Syntax/Quantifier.hs
@@ -42,7 +42,7 @@ import Language.Spectacle.Syntax.Quantifier.Internal
 -- returned so long as the given predicate is 'True' for all elements in the container, otherwise a spectacle exception
 -- is raised.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 forall :: (Foldable f, QuantifierIntro m) => f a -> (a -> m Bool) -> m Bool
 forall xs = forallIntro (toList xs)
 {-# INLINE forall #-}
@@ -51,7 +51,7 @@ forall xs = forallIntro (toList xs)
 -- which satisfies the given predicate will be returned. If there exists no element in the container that satisfies the
 -- predicate then an exception is raised.
 --
--- @since 0.1.0.0
+-- @since 1.0.0
 exists :: (Foldable f, QuantifierIntro m) => f a -> (a -> m Bool) -> m Bool
 exists xs = existsIntro (toList xs)
 {-# INLINE exists #-}
diff --git a/src/Language/Spectacle/Syntax/Quantifier/Internal.hs b/src/Language/Spectacle/Syntax/Quantifier/Internal.hs
index 5fa6d7c..702da71 100644
--- a/src/Language/Spectacle/Syntax/Quantifier/Internal.hs
+++ b/src/Language/Spectacle/Syntax/Quantifier/Internal.hs
@@ -25,7 +25,7 @@ class QuantifierIntro m where
 
   forallIntro :: [a] -> (a -> m Bool) -> m Bool
 
--- | @since 0.1.0.0
+-- | @since 1.0.0
 instance Member Quantifier effs => QuantifierIntro (Lang ctxt effs) where
   forallIntro xs p = scope (Forall xs p)
   {-# INLINE forallIntro #-}