diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,11 @@
+# Changelog for `experiments`
+
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
+and this project adheres to the
+[Haskell Package Versioning Policy](https://pvp.haskell.org/).
+
+## Unreleased
+
+## 0.1.0.0 - YYYY-MM-DD
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,26 @@
+Copyright 2025 Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1.  Redistributions of source code must retain the above copyright notice, this
+    list of conditions and the following disclaimer.
+
+2.  Redistributions in binary form must reproduce the above copyright notice,
+    this list of conditions and the following disclaimer in the documentation
+    and/or other materials provided with the distribution.
+
+3.  Neither the name of the copyright holder nor the names of its contributors
+    may be used to endorse or promote products derived from this software
+    without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/PropRatt.cabal b/PropRatt.cabal
new file mode 100644
--- /dev/null
+++ b/PropRatt.cabal
@@ -0,0 +1,86 @@
+cabal-version: 2.2
+name:           PropRatt
+version:        0.1.0.0
+synopsis:       Property-based testing framework for testing asynchronous FRP programs.
+category:       testing
+description:    
+                PropRatt is a property-based testing framework for testing Async Rattus programs.
+                The key component of PropRatt is its specification language, which extends basic linear temporal logic with
+                a means to express properties of several concurrent signals. This
+                allows users to express temporal properties that relate data coming from
+                different signals at different points in time.
+author:         Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr
+maintainer:     paba@itu.dk
+copyright:      2025 Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr
+license:        BSD-3-Clause
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    CHANGELOG.md
+
+source-repository head
+  type: git
+  location: https://github.com/pa-ba/PropRatt
+
+library
+  exposed-modules:
+      PropRatt
+      PropRatt.Arbitrary
+      PropRatt.Core
+      PropRatt.HList
+      PropRatt.LTL
+      PropRatt.Signal
+  other-modules:
+      PropRatt.Utils
+      PropRatt.Value
+  hs-source-dirs:
+      src
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
+  build-depends:
+      AsyncRattus >= 0.2 && < 0.3
+    , QuickCheck > 2.10 && < 3
+    , base >=4.7 && <5
+    , containers  >=0.6.5 && < 0.8
+  default-language: Haskell2010
+
+executable main-example
+  main-is: Main.hs
+  hs-source-dirs:
+      examples/main
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      AsyncRattus
+    , PropRatt
+    , QuickCheck
+    , base
+    , containers
+  default-language: Haskell2010
+
+executable timer-example
+  main-is: Timer.hs
+
+  hs-source-dirs:
+      examples/timer
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      AsyncRattus
+    , PropRatt
+    , QuickCheck
+    , base
+    , containers
+  default-language: Haskell2010
+
+test-suite PropRatt-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  hs-source-dirs:
+      test
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      AsyncRattus
+    , PropRatt
+    , QuickCheck
+    , base >=4.7 && <5
+    , containers
+  default-language: Haskell2010
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,8 @@
+# PropRatt
+
+PropRatt is a Haskell framework for testing AsyncRattus using property-based testing.
+
+# Running examples
+
+- `stack run main-example`
+- `stack run timer-example`
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/examples/main/Main.hs b/examples/main/Main.hs
new file mode 100644
--- /dev/null
+++ b/examples/main/Main.hs
@@ -0,0 +1,276 @@
+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+{-# LANGUAGE TypeApplications, FlexibleInstances #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# HLINT ignore "Use zipWith" #-}
+{-# HLINT ignore "Redundant bracket" #-}
+{-# HLINT ignore "Move brackets to avoid $" #-}
+{-# HLINT ignore "Use const" #-}
+
+module Main (main) where
+    
+import Test.QuickCheck
+import PropRatt
+import AsyncRattus.InternalPrimitives
+import Prelude hiding (zip, map, const)
+import AsyncRattus.Signal hiding (filter)
+import AsyncRattus.Strict hiding (singleton)
+import AsyncRattus.Plugin.Annotation
+import Prelude hiding (const, map, zip)
+import PropRatt.Signal
+import qualified Data.IntSet as IntSet
+
+{-# ANN module AllowLazyData #-}
+
+filterM :: Box (a -> Bool) -> Sig a -> Sig (Maybe' a)
+filterM f (x ::: xs) = if unbox f x
+  then Just' x ::: delay (filterM f (adv xs))
+  else Nothing' ::: delay (filterM f (adv xs))
+
+triggerM :: (Stable b) => Box (a -> b -> c) -> Sig a -> Sig b -> Sig (Maybe' c)
+triggerM f (a ::: as) bs@(b:::_) = Just' (unbox f a b) ::: triggerMAwait f as bs
+
+triggerMAwait :: Stable b => Box (a -> b -> c) -> O (Sig a) -> Sig b -> O (Sig (Maybe' c))
+triggerMAwait f as (b:::bs) = delay (case select as bs of
+            Fst (a' ::: as') bs' -> Just' (unbox f a' b) ::: triggerMAwait f as' (b ::: bs')
+            Snd as' bs' -> Nothing' ::: triggerMAwait f as' bs'
+            Both (a' ::: as') (b' ::: bs') -> Just' (unbox f a' b') ::: triggerMAwait f as' (b' ::: bs'))
+
+stutter :: (Stable a, Stable b) => Sig a -> Sig b -> Sig a
+stutter xs ys = map (box fst') (zip xs ys)
+
+monotonic :: (Stable a, Num a) => Sig a -> Sig a
+monotonic xs = scan (box (+)) 0 (map (box abs) xs)
+
+prop_interleave :: Property
+prop_interleave = forAll (generateSignals @[Int, Int]) $ \intSignals ->
+    let interleaved     = interleave (box (+)) (future $ first intSignals) (future $ second intSignals)
+        state           = prependLater interleaved $ flatten intSignals
+        predicate       = Next $ Always $ ((Now ((Index First) |==| (Index Second)))
+                                        `Or`
+                                        (Now ((Index First) |==| (Index Third))))
+                                        `Or`
+                                        (Now (((Index Second) + (Index Third)) |==| (Index First)))
+        result          = evaluate predicate state
+    in result
+
+-- Jumped signal should switch once the boxed predicate function is true.
+prop_jump :: Property
+prop_jump = forAll (generateSignals @Int) $ \intSignals ->
+   let  jumpFunc    = box (\n -> if n > 10 then Just' (const 1) else Nothing')
+        jumpSig     = jump jumpFunc (first intSignals)
+        state       = prepend jumpSig $ flatten intSignals
+        predicate   = Always $
+                        Now ((Index First) |==| (Index Second))
+                        `Or`
+                        Now ((Index First) |==| (Pure 1)) --
+        result      = evaluate predicate state
+    in result
+
+-- Prefix sum is strictly monotonically increasing, but fails for non-natural numbers.
+prop_scan_failing :: Property
+prop_scan_failing =  forAllShrink (generateSignals @Int) shrinkHls $ \intSignals ->
+    let prefixSum   = scan (box (+)) 0 (first intSignals)
+        state       = prepend prefixSum $ flatten intSignals
+        predicate   = Next $ Always $ Now $ Index (Previous First) |<| (Index First)
+        result      = evaluate predicate state
+    in counterexample ("Must be natural numbers.") result
+
+-- Prefix sum is strictly monotonically increasing is true for natural numbers.
+prop_scan :: Property
+prop_scan =  forAllShrink (generateSignals @Int) shrinkHls $ \intSignals ->
+    let absSig      = map (box (\x -> (abs x + 1))) (first intSignals)
+        prefixSum   = scan (box (+)) 0 absSig
+        state       = prepend prefixSum $ flatten intSignals
+        predicate   = Next $ Always $ Now $ Index (Previous First) |<| (Index First)
+        result      = evaluate predicate state
+    in result
+
+-- A switched signal has values equal to the first signal until its values equal values from the third signal
+prop_switchedSignal :: Property
+prop_switchedSignal = forAll (generateSignals @[Int, Int]) $ \intSignals ->
+    let switched    = switch (first intSignals) (future (second intSignals))
+        state       = prepend switched $ flatten intSignals
+        predicate   = Until (Now ((Index First) |==| (Index Second))) (Now ((Index First) |==| (Index Third)))
+        result      = evaluate predicate state
+    in result
+
+-- A buffered signal is always one tick behind.
+prop_buffer :: Property
+prop_buffer = forAll (generateSignals @Int) $ \intSignals ->
+    let bufferedSig = buffer 10 (first intSignals)
+        state       = prepend bufferedSig $ flatten intSignals
+        predicate   = Next $ Always $ Now $ (Index First) |==| Index (Previous Second)
+        result      = evaluate predicate state
+    in result
+
+-- A signal becomes constant once the predicate function to "stop" is true.
+prop_stop :: Property
+prop_stop = forAll (generateSignals @Int) $ \intSignals ->
+    let stopped     = stop (box (>100)) (first intSignals)
+        state       = prepend stopped $ flatten intSignals
+        predicate   = Always $ Implies (Now ((Index First) |>| (Pure 100))) (Always $ Next (Now (Index (Previous First) |==| (Index First))))
+        result      = evaluate predicate state
+    in result
+
+-- A zipped signal always has fst' values from second signal and snd' values from third signal.
+prop_zip :: Property
+prop_zip = forAll (generateSignals @[Int, Int]) $ \intSignals ->
+    let s1          = zip (first intSignals) (second intSignals)
+        state       = prepend s1 $ flatten intSignals
+        predicate   = Always $ Now ((fst' <$> (Index First)) |==| (Index Second)) `And` (Now ((snd' <$> (Index First)) |==| (Index Third)))
+        result      = evaluate predicate state
+    in result
+
+prop_filter :: Property
+prop_filter = forAll (generateSignals @Int) $ \intSignals ->
+  let filtered      = filterM (box (>= 10)) (first intSignals)
+      state         = prepend filtered $ flatten intSignals
+      predicate     = Always $ 
+            Implies (Now ((Index Second) |>=| Pure (10))) (Now ((Index First) |>=| (Pure (Just' 10))))
+            `And`
+            Implies (Now ((Index Second) |<| Pure (10))) (Now ((Index First) |==| (Pure Nothing')))
+      result        = evaluate predicate state
+  in result
+
+prop_triggerM :: Property
+prop_triggerM = forAll (generateSignals @[Int, Int]) $ \intSignals ->
+  let triggered     = triggerM (box (*)) (first intSignals) (second intSignals)
+      state         = prepend triggered $ flatten intSignals
+      predicate     = Always $ 
+            Implies (Now ((Ticked Second) |==| (Pure True))) ((Now ((Ticked First) |==| (Pure True))) `And` (Now ((fromMaybe' 0 <$> (Index First)) |==| ((Index Second) * (Index Third)))))
+      result        = evaluate predicate state
+  in result
+
+prop_parallel :: Property
+prop_parallel = forAllShrink (generateSignals @[Int, Int]) shrinkHls $ \intSignals ->
+    let paralleled  = parallel (first intSignals) (second intSignals)
+        state       = prepend paralleled $ flatten intSignals
+        predicate   = Always $
+            Implies (Now (Ticked Third)) (Now (Ticked First))
+            `And`
+            Implies (Now (Ticked Second)) (Now (Ticked First))
+        result      = evaluate predicate state
+    in result
+
+prop_isStuttering :: Property
+prop_isStuttering = forAll (generateSignals @[Int, Int]) $ \intSignals ->
+    let stuttered   = stutter (first intSignals) (second intSignals)
+        state       = prepend stuttered $ flatten intSignals
+        predicate   = Always $
+            Implies (Now (Ticked First)) (Now (Index First |==| Index Second))
+            `And`
+            Next (Implies (And (Now (Ticked Third)) (Not (Now (Ticked Second)))) (Now (Index (Previous First) |==| Index First)))
+        result      = evaluate predicate state
+    in result
+
+prop_functionIsMonotonic :: Property
+prop_functionIsMonotonic = forAll (generateSignals @Int) $ \intSignals ->
+    let mono        = monotonic (first intSignals)
+        state       = singletonH mono
+        predicate   = Always $ Next (Now ((Index First) |>=| (Index (Previous First))))
+        result      = evaluate predicate state
+    in result
+
+prop_singleSignalAlwaysTicks :: Property
+prop_singleSignalAlwaysTicks = forAllShrink (arbitrary :: Gen (Sig Int)) shrink $ \sig ->
+    let state       = singletonH sig
+        predicate   = Always $ Now ((Ticked First) |==| (Pure True))
+        result      = evaluate predicate state
+    in result
+
+-- Switched signal equals XS until YS has ticked, from then on the value is constant assuming ys has not produced another const signal
+prop_switchR :: Property
+prop_switchR = forAllShrink (generateSignals @Int) shrinkHls $ \intSignals ->
+    let xs                  = first intSignals
+        (_ ::: ys)          = (scan (box (\n _ -> n + 1)) 0 (takeN (sigLength xs) mkSigZero)) :: Sig Int
+        zs                  = switchR xs (mapAwait (box (\b _ -> const b)) ys)
+        state               = prepend zs $ prependLater ys $ flatten intSignals
+        predicate           = (Now ((Index First) |==| (Index Third)))
+                                `Until`
+                                (Now ((Ticked Second) |==| (Pure True)))
+                                `And` 
+                                ((Always $ Next 
+                                    (((Implies  (Not (Now (Ticked Second))) (Now ((Index (Previous First)) |==| (Index First))))))))
+                                `Until`
+                               (Next $ (Implies (Now (Ticked Second)) (Not (Now ((Index (Previous First)) |==| (Index First))))))
+        result              = evaluate predicate state
+    in counterexample (show state) result
+
+prop_switchS :: Property
+prop_switchS = forAllShrink (generateSignals @Int) shrinkHls $ \intSignals ->
+    let xs                  = first intSignals
+        gg@(_ ::: ys)       = (scan (box (\n _ -> n + 1)) 0 (takeN (sigLength xs) mkSigZero)) :: Sig Int
+        ggg                 = Delay (IntSet.fromList [1,2,3]) (\_ a -> const a)
+        zs                  = switchS xs ggg
+        state               = prepend zs $ prependLater ys $ flatten intSignals
+        predicate           =(Now ((Index First) |==| (Index Third)))
+                                `Until`
+                                (Now ((Ticked Second) |==| (Pure True)))
+                                `And` 
+                                ((Always $ Next 
+                                    (((Implies  (Not (Now (Ticked Second))) (Now ((Index (Previous First)) |==| (Index First))))))))
+                                `Until`
+                               (Next $ (Implies (Now (Ticked Second)) (Not (Now ((Index (Previous First)) |==| (Index First))))))
+        result              = evaluate predicate state
+    in counterexample (show gg ++ show zs ++ show xs) result
+
+prop_sigLength :: Property
+prop_sigLength = forAllShrink (arbitrary :: Gen (Sig Int)) shrink $ \(sig :: Sig Int) ->
+        let state       = singletonH (sig :: Sig Int)
+            predicate   = Always $ (Now ((Index First) |<| (Pure 50)))
+            result      = evaluate predicate state
+        in result
+
+prop_sigIsPositive :: Property
+prop_sigIsPositive = forAll (generateSignals @Int) $ \sig ->
+        let mapped      = map (box (abs)) (first sig)
+            state       = singletonH mapped
+            predicate   = Next $ Always $ Now ((Index (Prior 1 First)) |>=| (Pure 0))
+            result      = evaluate predicate state 
+        in result
+
+prop_catchsubtle :: Property
+prop_catchsubtle = forAllShrink (arbitrary :: Gen (Sig Int)) shrink $ \(sig :: Sig Int) ->
+        let state       = singletonH (sig :: Sig Int)
+            predicate   = Always $ Implies (Now ((Index First) |>| (Pure 80))) (Next $ (Now ((Index First) |<| (Index (Previous First)))))
+            result      = evaluate predicate state
+        in result
+
+prop_predLengthOutsideDefault :: Property
+prop_predLengthOutsideDefault =  forAllShrink (generateSignals @Int) shrinkHls $ \intSignals ->
+    let prefixSum   = scan (box (+)) 0 (first intSignals)
+        state       = prepend prefixSum $ flatten intSignals
+        predicate   = After 100 $ Always $ Now $ Index (Previous First) |<| (Index First)
+        result      = evaluate predicate state
+    in result
+
+main :: IO ()
+main = do
+    quickCheck prop_interleave
+    quickCheck prop_switchedSignal
+    quickCheck prop_buffer
+    quickCheck prop_zip
+    quickCheck prop_jump
+    quickCheck prop_stop
+    quickCheck prop_scan
+    quickCheck prop_filter
+    quickCheck prop_triggerM
+    quickCheck prop_parallel
+    quickCheck prop_isStuttering
+    quickCheck prop_functionIsMonotonic
+    quickCheck prop_singleSignalAlwaysTicks
+    quickCheck prop_sigIsPositive
+    quickCheck prop_switchS
+
+    putStrLn "=== Failing tests ==="
+    quickCheck prop_scan_failing
+    putStrLn "====================="
+    quickCheck prop_sigLength
+    putStrLn "====================="
+    quickCheck (withMaxSuccess 1000 prop_switchR)
+    putStrLn "====================="
+    quickCheck (withMaxSuccess 1000 prop_catchsubtle)
+    putStrLn "====================="
+    quickCheck prop_predLengthOutsideDefault
diff --git a/examples/timer/Timer.hs b/examples/timer/Timer.hs
new file mode 100644
--- /dev/null
+++ b/examples/timer/Timer.hs
@@ -0,0 +1,159 @@
+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Main (main) where
+
+import Test.QuickCheck
+import PropRatt
+import AsyncRattus.Strict
+import AsyncRattus.Signal
+import AsyncRattus.InternalPrimitives
+import Prelude hiding (map, const, zipWith, zip, filter, getLine, putStrLn,null, max)
+import qualified Data.IntSet as IntSet
+import AsyncRattus.Plugin.Annotation
+
+
+{-# ANN module AllowLazyData #-}
+
+{-# ANN everySecondSig AllowRecursion #-}
+everySecondSig :: O (Sig ())
+everySecondSig = Delay (IntSet.fromList [2]) (\_ -> () ::: everySecondSig)
+
+nats :: O (Sig ()) -> (Int :* Int) -> Sig (Int :* Int)
+nats later (n :* max) = stop
+    (box (\ (n' :* max') -> n' >= max'))
+    (scanAwait (box (\ (n' :* max') _ -> (n' + 1) :* max')) (n :* max) later)
+
+resetTuple :: (Int :* Int) -> (Int :* Int)
+resetTuple (_ :* max) = (0 :* max)
+
+setMax :: Int -> (Int :* Int) -> (Int :* Int)
+setMax max' (n :* _) = ((min n max') :* max')
+
+timerState :: Sig () -> Sig Int -> Sig (Int :* Int)
+timerState (_ ::: rr) sliderSig@(_ ::: ss) =
+    let     resetSig    = mapAwait (box (\ _ -> resetTuple)) rr
+            currentMax  = current sliderSig
+            setMaxSig   = mapAwait (box setMax) ss
+            inputSig    = interleave (box (.)) resetSig setMaxSig
+            inputSig'   = mapAwait (box ((nats everySecondSig) .)) inputSig
+            counterSig  = switchR ((nats everySecondSig) (0 :* currentMax)) inputSig'
+    in counterSig
+
+prop_counterSigAlwaysLessThanMax :: Property
+prop_counterSigAlwaysLessThanMax = forAll genDouble $ \(reset, slider) ->
+        let counterSig  = timerState reset slider
+            state       = prepend counterSig $ prepend reset $ singletonH slider
+            predicate   = Always $ Now ((fst' <$> Index First) |<=| (snd' <$> Index First))
+            result      = evaluate predicate state
+        in counterexample (show state) result
+  where
+    genDouble = do
+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))
+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))
+      return (reset, slider)
+
+prop_maxAlwaysEqualsMax :: Property
+prop_maxAlwaysEqualsMax = forAll genDouble $ \(reset, slider) ->
+        let counterSig  = timerState reset slider
+            state       = prepend counterSig $ prepend reset $ singletonH slider
+            predicate   = Always $ Now ((Index Third) |==| (snd' <$> Index First))
+            result      = evaluate predicate state
+        in counterexample (show state) result
+  where
+    genDouble = do
+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))
+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))
+      return (reset, slider)
+
+-- Concurrently resetting and dragging slider yields a reset signal with max value from slider.
+prop_concurrentResetAndSlider :: Property
+prop_concurrentResetAndSlider = forAll genDouble $ \(reset, slider) ->
+        let counterSig  = timerState reset slider
+            state       = prepend counterSig $ prepend reset $ singletonH slider
+            predicate   = Always $ Implies
+                (And (Now ((Ticked Second))) (Now ((Ticked Third))))
+                ((Now (((Index Third)) |==| (snd' <$> Index First)))
+                `And`
+                (Now ((Pure 0) |==| (fst' <$> Index First))))
+            result      = evaluate predicate state
+        in counterexample (show state) result
+  where
+    genDouble = do
+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))
+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))
+      return (reset, slider)
+
+prop_timerIsStrictlyMonotonicallyIncreasing :: Property
+prop_timerIsStrictlyMonotonicallyIncreasing = forAll genDouble $ \(reset, slider) ->
+        let counterSig  = timerState reset slider
+            state       = prepend counterSig $ prepend reset $ singletonH slider
+            predicate   = Always $ Next $
+                Implies
+                ((Now (Ticked First)) `And` ((Not (Now (Ticked Second)) `And` (Not (Now (Ticked Third))))))
+                (Now (((fst' <$> (Index First)) |>| (fst' <$> (Index (Previous First))))))
+            result      = evaluate predicate state
+        in counterexample (show state) result
+  where
+    genDouble = do
+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))
+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))
+      return (reset, slider)
+
+-- The initial state is set correctly.
+prop_init :: Property
+prop_init = forAll genDouble $ \(reset, slider) ->
+        let counterSig  = timerState reset slider
+            state       = prepend counterSig $ prepend reset $ singletonH slider
+            predicate   = Now ((fst' <$> (Index First)) |==| (Pure 0)) `And` (Now ((snd' <$> (Index First)) |==| (Index Third)))
+            result      = evaluate predicate state
+        in counterexample (show state) result
+  where
+    genDouble = do
+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))
+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))
+      return (reset, slider)
+
+-- If the counter signal hits the max value it remains at the max value until it is reset or slider has been moved.
+prop_counterSigStaysAtMaxValue :: Property
+prop_counterSigStaysAtMaxValue = forAllShrink genDouble shrink $ \(reset, slider) ->
+        let counterSig  = timerState reset slider
+            state       = prepend counterSig $ prepend reset $ singletonH slider
+            predicate   = Always $
+                Implies
+                    (Now ((fst' <$> (Index First)) |==| (snd' <$> (Index First))))
+                    (Next $ (Now ((fst' <$> (Index First)) |==| (fst' <$> (Index (Previous First))))
+                    `Until`
+                    ((Now (Ticked Second)) `Or` (Now (Ticked Third)))))
+            result      = evaluate predicate state
+        in counterexample (show state) result
+  where
+    genDouble = do
+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))
+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))
+      return (reset, slider)
+
+prop_counterSigAlwaysTicks :: Property
+prop_counterSigAlwaysTicks = forAll genDouble $ \(reset, slider) ->
+        let counterSig  = timerState reset slider
+            state       = prepend counterSig $ prepend reset $ singletonH slider
+            predicate   = Always $ Now (Ticked First) `And` (Next $ Now (Ticked First))
+            result      = evaluate predicate state
+        in counterexample (show state) result
+  where
+    genDouble = do
+      slider <- (arbitrarySigWith 100 (chooseInt (0, 100)) :: Gen (Sig Int))
+      reset <- (arbitrarySigWeighted 100 :: Gen (Sig (())))
+      return (reset, slider)
+
+main :: IO ()
+main = do
+    quickCheck prop_counterSigAlwaysLessThanMax
+    quickCheck prop_maxAlwaysEqualsMax
+    quickCheck prop_concurrentResetAndSlider
+    quickCheck prop_timerIsStrictlyMonotonicallyIncreasing
+    quickCheck prop_init
+    quickCheck prop_counterSigStaysAtMaxValue
+    quickCheck prop_counterSigAlwaysTicks
diff --git a/src/PropRatt.hs b/src/PropRatt.hs
new file mode 100644
--- /dev/null
+++ b/src/PropRatt.hs
@@ -0,0 +1,13 @@
+module PropRatt (
+    module PropRatt.Core,
+    module PropRatt.LTL,
+    module PropRatt.Arbitrary,
+    module PropRatt.HList,
+    module PropRatt.Utils
+) where
+
+import PropRatt.Core
+import PropRatt.LTL
+import PropRatt.Arbitrary
+import PropRatt.HList
+import PropRatt.Utils
diff --git a/src/PropRatt/Arbitrary.hs b/src/PropRatt/Arbitrary.hs
new file mode 100644
--- /dev/null
+++ b/src/PropRatt/Arbitrary.hs
@@ -0,0 +1,208 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# HLINT ignore "Use const" #-}
+
+module PropRatt.Arbitrary
+  ( arbitrarySig,
+    arbitrarySigWith,
+    arbitrarySigWeighted,
+    Sig (..),
+    generateSignals,
+    Map,
+    shrinkSignal,
+    shrinkHls
+  )
+where
+
+import AsyncRattus.InternalPrimitives
+import AsyncRattus.Plugin.Annotation
+import AsyncRattus.Signal hiding (map)
+import qualified Data.IntSet as IntSet
+import PropRatt.Utils
+import Data.Kind (Type)
+import Test.QuickCheck
+import Prelude hiding (const)
+import PropRatt.HList
+
+type TSig a = [(a, IntSet.IntSet)]
+
+instance (Arbitrary a) => Arbitrary (Sig a) where
+  arbitrary :: Gen (Sig a)
+  arbitrary = arbitrarySig 100
+  shrink :: Sig a -> [Sig a]
+  shrink sig = toSignal (shrinkSignal shrink sig)
+
+instance (Show a) => Show (Sig a) where
+  show :: Sig a -> String
+  show (x ::: xs) = show (toList (x ::: xs))
+
+instance (Eq a) => Eq (Sig a) where
+  (==) :: Sig a -> Sig a -> Bool
+  (==) sig1 sig2 = toList sig1 == toList sig2
+
+shrinkSignal :: (a -> [a]) -> Sig a -> [TSig a]
+shrinkSignal shr sig@(_ ::: (Delay cly _)) =
+  if IntSet.null cly
+    then shrinkOne testableSignal shr
+    else concat [ removes k n testableSignal | k <- takeWhile (>0) (iterate (`div`2) n) ]
+    ++ shrinkOne testableSignal shr
+  where
+    n = sigLength sig
+    testableSignal = toTSig sig
+
+{-# ANN shrinkOne AllowRecursion #-}
+shrinkOne :: TSig a -> (a -> [a]) -> [TSig a]
+shrinkOne [] _ = error "Testable signals are non-empty"
+shrinkOne [(x, cl)] shr = [ [(x', cl)] | x' <- shr x ]
+shrinkOne ((x, cl) : xs) shr = [ (x', cl) : xs | x'  <- shr x ] ++ [ (x, cl) : xs' | xs' <- shrinkOne xs shr ]
+
+{-# ANN removes AllowRecursion #-}
+removes :: Int -> Int -> TSig a -> [TSig a]
+removes k n tupleLs =
+  if k >= n
+    then []
+    else let xs1 = take k tupleLs
+             xs2 = drop k tupleLs
+         in xs1 : xs2 : map (xs1 ++) (removes k (n-k) xs2)
+
+{-# ANN toSignal AllowRecursion #-}
+toSignal :: [TSig a] -> [Sig a]
+toSignal [] = []
+toSignal [x] = [fromTSig x]
+toSignal (x : xs) = fromTSig x : toSignal xs
+
+{-# ANN fromTSig AllowRecursion #-}
+fromTSig :: TSig a -> Sig a
+fromTSig [] = error "Testable signals are non-empty"
+fromTSig [(x, _)] = x ::: never
+fromTSig ((x, cl) : xs) =
+  if IntSet.null cl
+    then x ::: never
+    else x ::: Delay cl (\_ -> fromTSig xs)
+
+{-# ANN toTSig AllowRecursion #-}
+toTSig :: Sig a -> TSig a
+toTSig (x ::: (Delay cl f)) =
+  if IntSet.null cl
+    then [(x, IntSet.empty)]
+    else (x, cl) : toTSig (f (InputValue (IntSet.findMin cl) ()))
+
+genClockChannelWeighted :: Gen Int
+genClockChannelWeighted = frequency [(1, pure 1), (1, pure 2), (50, pure 3)]
+
+genClock :: Int -> Gen Clock
+genClock n = case n of
+    1 -> do
+      x <- chooseInt (1,3)
+      return (IntSet.fromList [x])
+    2 -> frequency [(1, return (IntSet.fromList [1,2])),(1, return (IntSet.fromList [2,3])),(1, return (IntSet.fromList [1,3]))]
+    3 -> return (IntSet.fromList [1,2,3])
+    _ -> error "Partial function doesnt support n > 3"
+
+genClockListWeighted :: Gen [Int]
+genClockListWeighted = vectorOf 1 genClockChannelWeighted
+
+{-# ANN arbitrarySig AllowRecursion #-}
+arbitrarySig :: (Arbitrary a) => Int -> Gen (Sig a)
+arbitrarySig n = do
+  if n <= 0
+    then error "Cannot create empty signals"
+    else
+      go n
+      where
+        go 1 = do
+          x <- arbitrary
+          return (x ::: never)
+        go m = do
+          x <- arbitrary
+          len <- chooseInt (1, 3)
+          cl <- genClock len
+          xs <- go (m - 1)
+          let later = Delay cl (\_ -> xs)
+          return (x ::: later)
+
+{-# ANN arbitrarySigWith AllowRecursion #-}
+arbitrarySigWith :: Int -> Gen a -> Gen (Sig a)
+arbitrarySigWith n gen = do
+  if n <= 0
+    then error "Cannot create empty signals"
+    else
+      go n
+      where
+        go 1 = do
+          x <- gen
+          return (x ::: never)
+        go m = do
+          x <- gen
+          len <- chooseInt (1, 3)
+          cl <- genClock len
+          xs <- go (m - 1)
+          let later = Delay cl (\_ -> xs)
+          return (x ::: later)
+
+{-# ANN arbitrarySigWeighted AllowRecursion #-}
+arbitrarySigWeighted :: (Arbitrary a) => Int -> Gen (Sig a)
+arbitrarySigWeighted n = do
+  if n <= 0
+    then error "Cannot create empty signals"
+    else
+      go n
+      where
+        go 1 = do
+          x <- arbitrary
+          return (x ::: never)
+        go m = do
+          x <- arbitrary
+          cl <- genClockListWeighted
+          xs <- go (m - 1)
+          let later = Delay (IntSet.fromList cl) (\_ -> xs)
+          return (x ::: later)
+
+type family Map (f :: Type -> Type) (xs :: [Type]) :: [Type] where
+  Map f '[] = '[]
+  Map f (x ': xs) = f x ': Map f xs
+
+-- Use polykinds to allow us to overload generateSignals to work for both Type and Type -> Type
+type family ToList (a :: k) :: [Type] where
+  ToList (a :: [Type]) = a
+  ToList (a :: Type)   = '[a]
+
+class HListGen (ts :: [Type]) where
+  generateHList     :: Gen (HList (Map Sig ts))
+
+instance HListGen '[] where
+  generateHList = return HNil
+
+instance (Arbitrary (Sig t), HListGen ts) => HListGen (t ': ts) where
+  generateHList = do
+    x <- arbitrary
+    xs <- generateHList @ts
+    return (x %: xs)
+
+generateSignals :: forall a. HListGen (ToList a) => Gen (HList (Map Sig (ToList a)))
+generateSignals = generateHList @(ToList a)
+
+class ShrinkHList as where
+  shrinkHls :: HList as -> [HList as]
+
+instance ShrinkHList '[] where
+  shrinkHls _ = []
+
+instance (Arbitrary a, ShrinkHList as) => ShrinkHList (a ': as) where
+  shrinkHls (HCons x xs) =
+    [ HCons x' xs | x'  <- shrink x ] ++
+    [ HCons x xs' | xs' <- shrinkHls xs ] ++
+    [ HCons x' xs' | x'  <- shrink x, xs' <- shrinkHls xs ]
diff --git a/src/PropRatt/Core.hs b/src/PropRatt/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/PropRatt/Core.hs
@@ -0,0 +1,74 @@
+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+
+module PropRatt.Core (
+  prepend,
+  prependLater,
+  flatten,
+  singletonH
+) where
+
+import AsyncRattus.Signal
+import AsyncRattus.Strict hiding (singleton)
+import AsyncRattus.InternalPrimitives hiding (never)
+import PropRatt.Value
+import PropRatt.HList
+import Prelude hiding (const)
+
+emptySig :: Sig (HList '[])
+emptySig = const HNil
+
+class Stable (HList vals) => Flatten sigs vals | sigs -> vals, vals -> sigs where
+  flatten :: HList sigs -> Sig (HList vals)
+
+instance Flatten '[] '[] where
+  flatten :: HList '[] -> Sig (HList '[])
+  flatten HNil = emptySig
+
+instance (Stable a, Stable (Value a), Flatten as bs, Falsify bs) => Flatten (Sig a ': as) (Value a ': bs) where
+  flatten :: HList (Sig a : as) -> Sig (HList (Value a : bs))
+  flatten (HCons h t) = prepend h (flatten t)
+
+class Falsify ts where
+  toFalse :: HList ts -> HList ts
+
+instance Falsify '[] where
+  toFalse :: HList '[] -> HList '[]
+  toFalse _ =  HNil
+
+instance (Falsify ts) => Falsify (Value t ': ts) where
+  toFalse :: HList (Value t : ts) -> HList (Value t : ts)
+  toFalse (HCons (Current _ x) t) = Current (HasTicked False) x %: toFalse t
+
+-- | Like 'prepend', but the new head is delayed by one tick.
+--   This emits a dummy value at the head on the first tick, then behaves like 'prepend' on subsequent ticks.
+prependLater :: (Stable t, Stable (HList ts), Falsify ts) => O (Sig t) -> Sig (HList ts) -> Sig (HList (Value t ': ts))
+prependLater xs (y ::: ys) =
+  HCons (Current (HasTicked False) Nil) y ::: prependAwait Nil xs y ys
+
+prepend :: (Stable t, Stable (HList ts), Falsify ts) => Sig t -> Sig (HList ts) -> Sig (HList (Value t ': ts))
+prepend (x ::: xs) (y ::: ys) =
+  HCons (Current (HasTicked True) (x :! Nil)) y ::: prependAwait (x :! Nil) xs y ys
+
+prependAwait :: (Stable t, Stable hls, hls ~ HList ts, Falsify ts) => List t -> O (Sig t) -> hls -> O (Sig hls) -> O (Sig (HList (Value t ': ts)))
+prependAwait x xs y ys  = delay (
+  case select xs ys of
+     Fst (x' ::: xs')   ys'         -> (Current (HasTicked True) (x' :! x) %: toFalse y)  ::: prependAwait (x' :! x) xs' y ys'
+     Snd xs' (y' ::: ys')           -> (Current (HasTicked False) x %: y')                ::: prependAwait x xs' y' ys'
+     Both (x' ::: xs') (y' ::: ys') -> (Current (HasTicked True) (x' :! x) %: y')         ::: prependAwait (x' :! x) xs' y' ys')
+
+singletonH :: (Stable t) => Sig t -> Sig (HList '[Value t])
+singletonH sig = flatten (sig %: HNil)
diff --git a/src/PropRatt/HList.hs b/src/PropRatt/HList.hs
new file mode 100644
--- /dev/null
+++ b/src/PropRatt/HList.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
+module PropRatt.HList (HList(..), (%:), first,second,third,fourth,fifth,sixth,seventh,eighth,ninth,lengthH) where       
+import AsyncRattus.InternalPrimitives ( Stable )
+import Data.Kind (Type)
+
+data HList :: [Type] -> Type where
+  HNil :: HList '[]
+  HCons :: !x -> !(HList xs) -> HList (x ': xs)
+
+infixr 5 %:
+(%:) :: x -> HList xs -> HList (x ': xs)
+(%:) = HCons
+
+instance Show (HList '[]) where
+  show :: HList '[] -> String
+  show HNil = "HNil"
+
+instance (Show x, (Show (HList xs))) => Show (HList (x ': xs)) where
+  show :: (Show x, Show (HList xs)) => HList (x : xs) -> String
+  show (HCons x xs) = show x ++ " %: " ++ show xs
+
+instance Stable (HList '[]) where
+instance (Stable a, Stable (HList as)) => Stable (HList (a ': as)) where
+
+first :: HList (a ': _) -> a
+first (HCons h _) = h
+
+second :: HList (_ ': a ': _) -> a
+second (HCons _ (HCons h2 _)) = h2
+
+third :: HList (_ ': _ ': a ': _) -> a
+third (HCons _ (HCons _ (HCons h3 _))) = h3
+
+fourth :: HList (_ ': _ ': _ ': a ': _) -> a
+fourth (HCons _ (HCons _ (HCons _ (HCons h4 _)))) = h4
+
+fifth :: HList (_ ': _ ': _ ': _ ': a ': _) -> a
+fifth (HCons _ (HCons _ (HCons _ (HCons _ (HCons h5 _))))) = h5
+
+sixth :: HList (_ ': _ ': _ ': _ ': _ ': a ': _) -> a
+sixth (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h6 _)))))) = h6
+
+seventh :: HList (_ ':_ ': _ ': _ ': _ ': _ ': a ': _) -> a
+seventh (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h7 _))))))) = h7
+
+eighth :: HList (_ ': _ ': _ ': _ ': _ ': _ ': _ ': a ': _) -> a
+eighth (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h8 _)))))))) = h8
+
+ninth :: HList (_ ': _ ': _ ': _ ': _ ': _ ': _ ': _ ': a ': _) -> a
+ninth (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons _ (HCons h9 _))))))))) = h9
+
+
+lengthH :: HList ts -> Int -> Int
+lengthH HNil n = n
+lengthH (HCons _ as) n = lengthH as (n+1)
diff --git a/src/PropRatt/LTL.hs b/src/PropRatt/LTL.hs
new file mode 100644
--- /dev/null
+++ b/src/PropRatt/LTL.hs
@@ -0,0 +1,295 @@
+{-# LANGUAGE GADTs, DataKinds, MultiParamTypeClasses, RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module PropRatt.LTL
+  ( Pred (..),
+    evaluate,
+    evaluateWith,
+    Expr (..),
+    Lookup (..),
+    (|<|),
+    (|<=|),
+    (|>|),
+    (|>=|),
+    (|==|),
+  )
+where
+
+import AsyncRattus.InternalPrimitives
+import AsyncRattus.Strict
+import AsyncRattus.Signal hiding (const)
+import qualified Data.IntSet as IntSet
+import Data.Kind
+import PropRatt.Value
+import PropRatt.HList
+import PropRatt.Utils
+
+data Pred (ts :: [Type]) where
+  Tautology     :: Pred ts
+  Contradiction :: Pred ts
+  Now           :: Expr ts Bool -> Pred ts
+  Not           :: Pred ts -> Pred ts
+  And           :: Pred ts -> Pred ts -> Pred ts
+  Or            :: Pred ts -> Pred ts -> Pred ts
+  Until         :: Pred ts -> Pred ts -> Pred ts
+  Next          :: Pred ts -> Pred ts
+  Implies       :: Pred ts -> Pred ts -> Pred ts
+  Always        :: Pred ts -> Pred ts
+  Eventually    :: Pred ts -> Pred ts
+  After         :: Int -> Pred ts-> Pred ts
+  Release       :: Pred ts -> Pred ts -> Pred ts
+
+data Expr (ts :: [Type]) (t :: Type) where
+  Pure    :: t -> Expr ts t
+  Apply   :: Expr ts (t -> r) -> Expr ts t -> Expr ts r
+  Index   :: Lookup ts t -> Expr ts t
+  Ticked  :: Lookup ts t -> Expr ts Bool
+
+data Lookup (ts :: [Type]) (t :: Type) where
+  Previous  :: Lookup ts t -> Lookup ts t
+  Prior     :: Int -> Lookup ts t -> Lookup ts t
+  First     :: Lookup (Value t ': x) t
+  Second    :: Lookup (x1 ': Value t ': x2) t
+  Third     :: Lookup (x1 ': x2 ': Value t ': x3) t
+  Fourth    :: Lookup (x1 ': x2 ': x3 ': Value t ': x4) t
+  Fifth     :: Lookup (x1 ': x2 ': x3 ': x4 ': Value t ': x5) t
+  Sixth     :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': Value t ': x6) t
+  Seventh   :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': Value t ': x7) t
+  Eighth    :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': x7 ': Value t ': x8) t
+  Ninth     :: Lookup (x1 ': x2 ': x3 ': x4 ': x5 ': x6 ': x7 ': x8 ': Value t ': x9) t
+
+instance Functor (Expr ts) where
+  fmap :: (t -> r) -> Expr ts t -> Expr ts r
+  fmap f (Pure x)     = Pure (f x)
+  fmap f (Apply g x)  = Apply (fmap (f .) g) x
+  fmap f (Index lu)   = Apply (Pure f) (Index lu)
+  fmap f (Ticked lu)  = Apply (Pure f) (Ticked lu)
+
+instance Applicative (Expr ts) where
+    pure :: t -> Expr ts t
+    pure = Pure
+    (<*>) :: Expr ts (t -> r) -> Expr ts t -> Expr ts r
+    Pure f <*> x = fmap f x
+    Apply f g <*> x = Apply (Apply f g) x
+    (<*>) _ _ = error "Expr: unsupported constructor for applicative application."
+
+instance Num t => Num (Expr ts t) where
+  (+) :: Expr ts t -> Expr ts t -> Expr ts t
+  (+) x y = (+) <$> x <*> y
+  (-) :: Expr ts t -> Expr ts t -> Expr ts t
+  (-) x y = (-) <$> x <*> y
+  (*) :: Expr ts t -> Expr ts t -> Expr ts t
+  (*) x y = (*) <$> x <*> y
+  negate :: Expr ts t -> Expr ts t
+  negate = fmap negate
+  abs :: Expr ts t -> Expr ts t
+  abs = fmap abs
+  signum :: Expr ts t -> Expr ts t
+  signum = fmap signum
+  fromInteger :: Integer -> Expr ts t
+  fromInteger n = pure (fromInteger n)
+
+(|<|) :: (Applicative f, Ord t) => f t -> f t -> f Bool
+x |<| y = (<) <$> x <*> y
+(|<=|) :: (Applicative f, Ord t) => f t -> f t -> f Bool
+x |<=| y = (<=) <$> x <*> y
+(|>|) :: (Applicative f, Ord t) => f t -> f t -> f Bool
+x |>| y = (>) <$> x <*> y
+(|>=|) :: (Applicative f, Ord t) => f t -> f t -> f Bool
+x |>=| y = (>=) <$> x <*> y
+(|==|) :: (Applicative f, Eq t) => f t -> f t -> f Bool
+x |==| y = (==) <$> x <*> y
+
+-- | Checks whether the instances of "previous" is within scope of t "next" operator.
+-- This prevents the evaluation from looking too far back in time.
+checkScope :: Pred ts -> Bool
+checkScope p = checkPred p 0
+
+-- | Traverses the predicate supplied and exits early if it finds a subtree where the scope is negative.
+-- The scope is incremented for each next constructor, and decremented for each previous or prior constructor.
+checkPred :: Pred ts -> Int -> Bool
+checkPred predicate scope =
+  valid scope &&
+  case predicate of
+    Tautology       -> valid scope
+    Contradiction   -> valid scope
+    Now expr        -> valid (checkExpr expr scope)
+    Not p           -> checkPred p scope
+    And p1 p2       -> checkPred p1 scope && checkPred p2 scope
+    Or p1 p2        -> checkPred p1 scope || checkPred p2 scope
+    Until p1 p2     -> checkPred p1 scope && checkPred p2 scope
+    Next p          -> checkPred p (scope + 1)
+    Implies p1 p2   -> checkPred p1 scope && checkPred p2 scope
+    Release p1 p2   -> checkPred p1 scope && checkPred p2 scope
+    Always p        -> checkPred p scope
+    Eventually p    -> checkPred p scope
+    After n p       -> checkPred p (scope + n)
+  where
+    valid s = s >= 0
+
+-- | Propegates the smallest scope found by traversing the expr.
+checkExpr :: Expr ts t -> Int -> Int
+checkExpr expr scope =
+  case expr of
+    Pure _        -> scope
+    Apply fun arg -> min (checkExpr fun scope) (checkExpr arg scope)
+    Index lu      -> checkLookup lu scope
+    Ticked lu     -> checkLookup lu scope
+
+checkLookup :: Lookup ts t -> Int -> Int
+checkLookup lu scope =
+  case lu of
+    Previous lu'  -> checkLookup lu' (scope - 1)
+    Prior n lu'   -> checkLookup lu' (scope - n)
+    _             -> scope
+
+-- Returns the amount of signal elements needed to evaluate the predicate.
+minSigLengthForPred :: Pred ts -> Int -> Int
+minSigLengthForPred predicate acc =
+    case predicate of
+      Not p           -> minSigLengthForPred p acc
+      And p1 p2       -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
+      Or p1 p2        -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
+      Until p1 p2     -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
+      Next p          -> minSigLengthForPred p (acc + 1)
+      Implies p1 p2   -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
+      Release p1 p2   -> minSigLengthForPred p1 acc `max` minSigLengthForPred p2 acc
+      Always p        -> minSigLengthForPred p acc
+      Eventually p    -> minSigLengthForPred p acc
+      After n p       -> minSigLengthForPred p (acc + n)
+      _               -> acc
+
+nthPrevious :: Int -> Value t -> Maybe' (Value t)
+nthPrevious n curr@(Current b history)
+  | n <= 0    = Just' curr
+  | otherwise =
+      case history of
+        _ :! xs -> nthPrevious (n - 1) (Current b xs)
+        Nil     -> Nothing'
+
+evalTicked :: Lookup ts t -> HList ts -> Bool
+evalTicked lu hls = case lu of
+  Previous _ -> errorTickedPast
+  Prior _ _  -> errorTickedPast
+  First      -> extract $ first hls
+  Second     -> extract $ second hls
+  Third      -> extract $ third hls
+  Fourth     -> extract $ fourth hls
+  Fifth      -> extract $ fifth hls
+  Sixth      -> extract $ sixth hls
+  Seventh    -> extract $ seventh hls
+  Eighth     -> extract $ eighth hls
+  Ninth      -> extract $ ninth hls
+  where
+    errorTickedPast                   = error "Cannot check if signal has ticked in the past."
+    extract (Current (HasTicked b) _) = b
+
+evalExpr :: Expr ts t -> HList ts -> Expr ts t
+evalExpr (Pure x) _      = pure x
+evalExpr (Apply f x) hls = (($) <$> evalExpr f hls) <*> evalExpr x hls
+evalExpr (Index lu) hls  =
+  case evalLookup lu hls of
+    Just' (Current _ (h :! _)) -> pure h
+    Just' (Current _ Nil)      -> error "History not found for signal."
+    Nothing'                   -> error "Signal not found."
+evalExpr (Ticked lu) hls = pure (evalTicked lu hls)
+
+evalLookup :: Lookup ts t -> HList ts -> Maybe' (Value t)
+evalLookup lu hls = case lu of
+  Previous lu' ->
+    case evalLookup lu' hls of
+      Just' (Current b history) ->
+        case history of
+          _ :! xs -> Just' (Current b xs)
+          Nil     -> Nothing'
+      Nothing' -> Nothing'
+  Prior n lu'  -> case evalLookup lu' hls of
+    Just' v  -> nthPrevious n v
+    Nothing' -> Nothing'
+  First         -> Just' (first hls)
+  Second        -> Just' (second hls)
+  Third         -> Just' (third hls)
+  Fourth        -> Just' (fourth hls)
+  Fifth         -> Just' (fifth hls)
+  Sixth         -> Just' (sixth hls)
+  Seventh       -> Just' (seventh hls)
+  Eighth        -> Just' (eighth hls)
+  Ninth         -> Just' (ninth hls)
+
+-- Evaluate a single timestep. Used exclusively for shrink cases.
+evaluateSingle  :: Int -> Pred ts -> Sig (HList ts) -> Bool
+evaluateSingle timestepsLeft formulae sig@(x ::: _) =
+  timestepsLeft <= 0 || case formulae of
+            Tautology       -> True
+            Contradiction   -> False
+            Now expr        ->
+              case evalExpr expr x of
+                Pure b -> b
+                _ -> error "Unexpected error during evaluation."
+            Not phi         -> not (eval phi sig)
+            And phi psi     -> eval phi sig && eval psi sig
+            Or phi psi      -> eval phi sig || eval psi sig
+            Until phi psi   -> eval psi sig || eval phi sig
+            Next _          -> True
+            Implies phi psi -> not (eval phi sig && not (eval psi sig))
+            Always phi      -> eval phi sig
+            Eventually phi  -> eval phi sig 
+            Release _ _     -> True 
+            After _ _       -> True
+        where
+          eval = evaluateSingle timestepsLeft
+
+evaluate' :: Int -> Pred ts -> Sig (HList ts) -> Bool
+evaluate' timestepsLeft formulae sig@(x ::: Delay cl f) =
+  if IntSet.null cl
+    then evaluateSingle timestepsLeft formulae sig
+    else timestepsLeft <= 0 || case formulae of
+            Tautology       -> True
+            Contradiction   -> False
+            Now expr        ->
+              case evalExpr expr x of
+                Pure b -> b
+                _ -> error "Unexpected error during evaluation."
+            Not phi         -> not (eval phi sig)
+            And phi psi     -> eval phi sig && eval psi sig
+            Or phi psi      -> eval phi sig || eval psi sig
+            Until phi psi   -> eval psi sig
+                              || (eval phi sig && evaluateNext (phi `Until` psi) advance)
+            Next phi        -> evaluateNext phi advance
+            Implies phi psi -> not (eval phi sig && not (eval psi sig))
+            Always phi      -> eval phi sig && evaluateNext (Always phi) advance
+            Eventually phi  -> (eval phi sig || evaluateNext (Eventually phi) advance)
+                                && not (timestepsLeft == 1 && not (eval phi sig))
+            Release phi psi -> (eval psi sig && eval phi sig)
+                                || (eval psi sig && evaluateNext (phi `Until` psi) advance)
+            After n phi     -> if n <= 0 then eval phi sig else evaluateNext (After (n - 1) phi) sig
+      where
+        evaluateNext = evaluate' (timestepsLeft - 1)
+        eval = evaluate' timestepsLeft
+        advance = f (InputValue (IntSet.findMin cl) ())
+
+-- Finds the minimum length a signal must have for the pred to be tested.
+-- If the length of the signal is too short, short circuit evaluation to true (shrink cases).
+evaluate :: Pred ts -> Sig (HList ts) -> Bool
+evaluate = evaluateWith 100
+
+evaluateWith :: Int -> Pred ts -> Sig (HList ts) -> Bool
+evaluateWith defaultTimeStepsToCheck p sig =
+  let len       = sigLength sig
+      min'      = minSigLengthForPred p 1
+      tooShort  = len < min'
+      scopeOk   = checkScope p
+  in 
+    if not scopeOk
+      then error "Previous must be in scope of next" 
+    else if min' > defaultTimeStepsToCheck
+      then error ("Cannot evaluate more than " ++ show defaultTimeStepsToCheck ++ " values.\n" ++ "Predicate requires " ++ show min' ++ " timesteps. Consider using evaluateWith (>= " ++ show min' ++ ")")
+    else
+      tooShort || evaluate' (defaultTimeStepsToCheck `min` len) p sig
diff --git a/src/PropRatt/Signal.hs b/src/PropRatt/Signal.hs
new file mode 100644
--- /dev/null
+++ b/src/PropRatt/Signal.hs
@@ -0,0 +1,15 @@
+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+
+module PropRatt.Signal (hlistLen,takeN) where
+
+import AsyncRattus.Signal
+import AsyncRattus
+import PropRatt.HList
+
+hlistLen :: Sig (HList ts) -> Int
+hlistLen (m ::: _) = lengthH m 0
+
+{-# ANN takeN AllowRecursion #-}
+takeN :: Int -> Sig a -> Sig a
+takeN 1 (x ::: _) = x ::: never
+takeN n (x ::: later) = x ::: delay (takeN (n-1) (adv later))
diff --git a/src/PropRatt/Utils.hs b/src/PropRatt/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/PropRatt/Utils.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# HLINT ignore "Use const" #-}
+{-# LANGUAGE GADTs #-}
+
+module PropRatt.Utils (smallest,toList,toListWithClock,toListOfLength,lengthSig,sigLength,mkSigOne,mkSigZero) where
+
+import AsyncRattus.Signal (Sig(..))
+import AsyncRattus.InternalPrimitives
+import qualified Data.IntSet as IntSet
+import Prelude hiding (map, zip, zipWith, take)
+
+
+smallest :: IntSet.IntSet -> Int
+smallest = IntSet.findMin
+
+
+toList :: Sig a -> [a]
+toList (x ::: Delay cl f)
+    | IntSet.null cl = [x]
+    | otherwise = x : toList (f (InputValue (smallest cl) ()))
+
+
+toListWithClock :: Sig a -> [(a, IntSet.IntSet)]
+toListWithClock (x ::: Delay cl f)
+    | IntSet.null cl = [(x, cl)]
+    | otherwise = (x, cl) : toListWithClock (f (InputValue (smallest cl) ()))
+
+
+toListOfLength :: Int -> Sig a -> [a]
+toListOfLength 0 _ = []
+toListOfLength n (x ::: Delay cl f) = x : toListOfLength (n-1) (f (InputValue (smallest cl) ()))
+
+
+lengthSig :: Sig a -> Int -> Int
+lengthSig (_ ::: Delay cl f) acc
+    | IntSet.null cl = acc + 1
+    | otherwise = lengthSig (f (InputValue (smallest cl) ())) (acc+1)
+
+sigLength :: Sig a -> Int
+sigLength sig = lengthSig sig 0
+
+
+
+mkSigOne :: Sig Int
+mkSigOne = 1 ::: Delay (IntSet.fromList [1]) (\_ -> mkSigOne)
+
+
+
+mkSigZero :: Sig Int
+mkSigZero = 0 ::: Delay (IntSet.fromList [2]) (\_ -> mkSigZero)
+
diff --git a/src/PropRatt/Value.hs b/src/PropRatt/Value.hs
new file mode 100644
--- /dev/null
+++ b/src/PropRatt/Value.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ScopedTypeVariables, UndecidableInstances #-}
+
+module PropRatt.Value (Value(..),pureVal,current, HasTicked(..)) where
+import AsyncRattus.Strict
+import AsyncRattus.Signal hiding (current)
+import PropRatt.Utils
+import AsyncRattus
+
+newtype HasTicked = HasTicked Bool deriving Show
+
+data Value a where
+  Current :: !HasTicked -> !(List a) -> Value a
+
+instance Stable (Value a) where 
+instance Num a => Num (Value a) where
+  (+) v1 v2 = pureVal (current v1 + current v2)
+  (-) v1 v2 = pureVal (current v1 - current v2)
+  (*) v1 v2 = pureVal (current v1 * current v2)
+  negate v  = pureVal (negate (current v))
+  abs v     = pureVal (abs (current v))
+  signum v  = pureVal (signum (current v))
+  fromInteger n = pureVal (fromInteger n)
+
+instance Show a => Show (Value a) where
+  show (Current t Nil) = show t
+  show (Current _ (h :! Nil)) = show h
+  show (Current _ (h :! h2 :! _)) =  show h ++ " " ++ show h2
+
+instance Show a => Show (Sig [Value a]) where
+  show sig = "Sig [Value a]: " ++ show (toListOfLength 100 sig) ++ "..."
+
+instance Ord a => Ord (Value a) where
+  compare v1 v2 = compare (current v1) (current v2)
+
+instance Eq a => Eq (Value a) where
+  v1 == v2 = current v1 == current v2
+
+pureVal :: a -> Value a
+pureVal x = Current (HasTicked False) (x :! Nil)
+
+current :: Value a -> a
+current (Current _ (h :! _)) = h
+current _ = undefined
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,23 @@
+{-# OPTIONS -fplugin=AsyncRattus.Plugin #-}
+{-# LANGUAGE TypeApplications, FlexibleInstances #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+import Test.QuickCheck
+import PropRatt.Arbitrary
+import PropRatt.Core
+import PropRatt.HList
+import PropRatt.Signal
+
+prop_shouldAddToHList :: Property
+prop_shouldAddToHList = forAll (generateSignals @[Int, Int]) $ \intSignals ->
+    let flat        = flatten intSignals
+        before      = hlistLen flat
+        state       = prepend (first intSignals) $ flatten intSignals
+        after       = hlistLen state
+        result      = (before + 1) == after
+    in result
+
+main :: IO ()
+main = do
+    quickCheck prop_shouldAddToHList