diff --git a/copilot-language.cabal b/copilot-language.cabal
--- a/copilot-language.cabal
+++ b/copilot-language.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-language
-version:             2.1.1
+version:             2.1.2
 synopsis:            A Haskell-embedded DSL for monitoring hard real-time
                      distributed systems.
 description:
@@ -32,11 +32,11 @@
   default-language: Haskell2010
   hs-source-dirs: src
   build-depends: array
-               , base >= 4.0 && <= 5.0
+               , base >= 4.0 && < 5
                , containers >= 0.4
-               , mtl >= 2.0
                , data-reify >= 0.6
---               , ghc-prim,
+               , mtl >= 2.0 && < 3
+               , ghc-prim >= 0.2
                , copilot-core >= 0.1
   exposed-modules: Copilot
                  , Copilot.Language
diff --git a/src/Copilot/Language.hs b/src/Copilot/Language.hs
--- a/src/Copilot/Language.hs
+++ b/src/Copilot/Language.hs
@@ -4,7 +4,7 @@
 
 -- | Main Copilot language export file.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Language
   ( module Data.Int
@@ -29,6 +29,7 @@
   , observer
   , trigger
   , arg
+  , prop
   , prettyPrint
   ) where
 
@@ -51,7 +52,8 @@
 import Copilot.Language.Operators.BitWise
 import Copilot.Language.Reify
 import Copilot.Language.Prelude
-import Copilot.Language.Spec (Spec, trigger, arg, observer)
+import Copilot.Language.Spec
+  (Spec, trigger, arg, observer, prop)
 import Copilot.Language.Stream (Stream)
 
 --------------------------------------------------------------------------------
diff --git a/src/Copilot/Language/Analyze.hs b/src/Copilot/Language/Analyze.hs
--- a/src/Copilot/Language/Analyze.hs
+++ b/src/Copilot/Language/Analyze.hs
@@ -2,7 +2,7 @@
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 --------------------------------------------------------------------------------
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
diff --git a/src/Copilot/Language/Operators/BitWise.hs b/src/Copilot/Language/Operators/BitWise.hs
--- a/src/Copilot/Language/Operators/BitWise.hs
+++ b/src/Copilot/Language/Operators/BitWise.hs
@@ -4,7 +4,7 @@
 
 -- | Bitwise operators.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 module Copilot.Language.Operators.BitWise
diff --git a/src/Copilot/Language/Operators/Boolean.hs b/src/Copilot/Language/Operators/Boolean.hs
--- a/src/Copilot/Language/Operators/Boolean.hs
+++ b/src/Copilot/Language/Operators/Boolean.hs
@@ -4,7 +4,7 @@
 
 -- | Boolean operators.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Language.Operators.Boolean
   ( (&&)
diff --git a/src/Copilot/Language/Operators/Cast.hs b/src/Copilot/Language/Operators/Cast.hs
--- a/src/Copilot/Language/Operators/Cast.hs
+++ b/src/Copilot/Language/Operators/Cast.hs
@@ -4,7 +4,7 @@
 
 -- | Type-safe casting operators.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 
 module Copilot.Language.Operators.Cast 
diff --git a/src/Copilot/Language/Operators/Constant.hs b/src/Copilot/Language/Operators/Constant.hs
--- a/src/Copilot/Language/Operators/Constant.hs
+++ b/src/Copilot/Language/Operators/Constant.hs
@@ -4,7 +4,7 @@
 
 -- | Constants.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Language.Operators.Constant
   ( constant
diff --git a/src/Copilot/Language/Operators/Eq.hs b/src/Copilot/Language/Operators/Eq.hs
--- a/src/Copilot/Language/Operators/Eq.hs
+++ b/src/Copilot/Language/Operators/Eq.hs
@@ -4,7 +4,7 @@
 
 -- | Equality operator.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Language.Operators.Eq
   ( (==)
diff --git a/src/Copilot/Language/Operators/Extern.hs b/src/Copilot/Language/Operators/Extern.hs
--- a/src/Copilot/Language/Operators/Extern.hs
+++ b/src/Copilot/Language/Operators/Extern.hs
@@ -4,7 +4,7 @@
 
 -- | External variables, arrays, and functions.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Language.Operators.Extern
   ( extern
diff --git a/src/Copilot/Language/Operators/Integral.hs b/src/Copilot/Language/Operators/Integral.hs
--- a/src/Copilot/Language/Operators/Integral.hs
+++ b/src/Copilot/Language/Operators/Integral.hs
@@ -4,7 +4,7 @@
 
 -- | Integral class operators.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Language.Operators.Integral
   ( div
diff --git a/src/Copilot/Language/Operators/Local.hs b/src/Copilot/Language/Operators/Local.hs
--- a/src/Copilot/Language/Operators/Local.hs
+++ b/src/Copilot/Language/Operators/Local.hs
@@ -4,7 +4,7 @@
 
 -- | Let expressions.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Language.Operators.Local
   ( local
diff --git a/src/Copilot/Language/Operators/Mux.hs b/src/Copilot/Language/Operators/Mux.hs
--- a/src/Copilot/Language/Operators/Mux.hs
+++ b/src/Copilot/Language/Operators/Mux.hs
@@ -4,7 +4,7 @@
 
 -- | if-then-else.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Language.Operators.Mux
   ( mux
diff --git a/src/Copilot/Language/Operators/Ord.hs b/src/Copilot/Language/Operators/Ord.hs
--- a/src/Copilot/Language/Operators/Ord.hs
+++ b/src/Copilot/Language/Operators/Ord.hs
@@ -4,7 +4,7 @@
 
 -- | Comparison operators.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Language.Operators.Ord
   ( (<=)
diff --git a/src/Copilot/Language/Operators/Temporal.hs b/src/Copilot/Language/Operators/Temporal.hs
--- a/src/Copilot/Language/Operators/Temporal.hs
+++ b/src/Copilot/Language/Operators/Temporal.hs
@@ -4,7 +4,7 @@
 
 -- | Stream construction.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 
 module Copilot.Language.Operators.Temporal
   ( (++)
diff --git a/src/Copilot/Language/Reify.hs b/src/Copilot/Language/Reify.hs
--- a/src/Copilot/Language/Reify.hs
+++ b/src/Copilot/Language/Reify.hs
@@ -5,7 +5,7 @@
 -- | Transforms a Copilot Language specification into a Copilot Core
 -- specification.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE ExistentialQuantification, Rank2Types #-}
 
 module Copilot.Language.Reify
@@ -33,19 +33,22 @@
 reify spec =
   do 
     analyze spec
-    let trigs = triggers  $ runSpec spec
-    let obsvs = observers $ runSpec spec
-    refMkId      <- newIORef 0
-    refVisited    <- newIORef M.empty
-    refMap        <- newIORef []
-    coreTriggers  <- mapM (mkTrigger  refMkId refVisited refMap) trigs
-    coreObservers <- mapM (mkObserver refMkId refVisited refMap) obsvs
-    coreStreams   <- readIORef refMap
+    let trigs = triggers   $ runSpec spec
+    let obsvs = observers  $ runSpec spec
+    let props = properties $ runSpec spec
+    refMkId         <- newIORef 0
+    refVisited      <- newIORef M.empty
+    refMap          <- newIORef []
+    coreTriggers    <- mapM (mkTrigger  refMkId refVisited refMap) trigs
+    coreObservers   <- mapM (mkObserver refMkId refVisited refMap) obsvs
+    coreProperties  <- mapM (mkProperty refMkId refVisited refMap) props
+    coreStreams     <- readIORef refMap
     return $
       Core.Spec
-        { Core.specStreams   = reverse coreStreams
-        , Core.specObservers = coreObservers
-        , Core.specTriggers  = coreTriggers }
+        { Core.specStreams    = reverse coreStreams
+        , Core.specObservers  = coreObservers
+        , Core.specTriggers   = coreTriggers
+        , Core.specProperties = coreProperties }
 
 --------------------------------------------------------------------------------
 
@@ -88,6 +91,22 @@
   mkTriggerArg (Arg e) = do
       w <- mkExpr refMkId refStreams refMap e
       return $ Core.UExpr typeOf w
+
+--------------------------------------------------------------------------------
+
+{-# INLINE mkProperty #-}
+mkProperty
+  :: IORef Int
+  -> IORef (Map Core.Id)
+  -> IORef [Core.Stream]
+  -> Property
+  -> IO Core.Property
+mkProperty refMkId refStreams refMap (Property name guard) = do
+    w1 <- mkExpr refMkId refStreams refMap guard 
+    return $
+      Core.Property
+        { Core.propertyName  = name
+        , Core.propertyExpr  = w1 }
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Copilot/Language/Spec.hs b/src/Copilot/Language/Spec.hs
--- a/src/Copilot/Language/Spec.hs
+++ b/src/Copilot/Language/Spec.hs
@@ -4,7 +4,7 @@
 
 -- | Copilot specifications.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 
@@ -19,6 +19,9 @@
   , triggers
   , trigger
   , arg
+  , Property (..)
+  , prop
+  , properties
   ) where
 
 import Control.Monad.Writer
@@ -57,16 +60,36 @@
       TriggerItem t -> t : ls
       _             -> ls
 
+properties :: [SpecItem] -> [Property]
+properties =
+  foldl' properties' []
+  where
+  properties' ls e =
+    case e of
+      PropertyItem p -> p : ls
+      _              -> ls
+
 --------------------------------------------------------------------------------
 
 data SpecItem
   = ObserverItem Observer
   | TriggerItem  Trigger
+  | PropertyItem Property
 
 --------------------------------------------------------------------------------
 
 data Observer where
   Observer :: Typed a => String -> Stream a -> Observer
+
+--------------------------------------------------------------------------------
+
+data Property where
+  Property :: String -> Stream Bool -> Property
+
+--------------------------------------------------------------------------------
+
+prop :: String -> Stream Bool -> Spec
+prop name e = tell [PropertyItem $ Property name e]
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Copilot/Language/Stream.hs b/src/Copilot/Language/Stream.hs
--- a/src/Copilot/Language/Stream.hs
+++ b/src/Copilot/Language/Stream.hs
@@ -4,7 +4,7 @@
 
 -- | Abstract syntax for streams and operators.
 
-{-# LANGUAGE Safe #-}
+{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE Rank2Types #-}