diff --git a/Control/Invariant.hs b/Control/Invariant.hs
new file mode 100644
--- /dev/null
+++ b/Control/Invariant.hs
@@ -0,0 +1,252 @@
+{-# LANGUAGE CPP, FlexibleInstances, StandaloneDeriving, TypeFamilies #-}
+module Control.Invariant
+    ( HasInvariant(..), Checked, IsChecked(..)
+    , mutate, mutate', create'
+    , Controls(..)
+    , view',(!.), views'
+    , use', uses'
+    , HasPrefix(..)
+    , (===), isSubsetOf', isProperSubsetOf'
+    , relation
+    , trading, holds
+    , invariantMessage
+    , provided, providedM
+    , assertFalse'
+    , Pre
+    , IsAssertion(..)
+    , checkAssert
+    , checkAssertM
+    , Invariant, (##)
+    , member'
+    , isSubmapOf' 
+    , isProperSubmapOf' )
+where
+
+import Control.DeepSeq
+import Control.Lens
+import Control.Monad.State
+import Control.Monad.RWS
+import Control.Precondition
+
+import Data.Default
+import Data.Functor.Compose
+import Data.Functor.Classes
+import Data.List
+import Data.Map (isSubmapOf,isProperSubmapOf,Map,member)
+import Data.Set (isSubsetOf,isProperSubsetOf,Set)
+import Data.Typeable
+
+import GHC.Stack.Utils
+
+import Test.QuickCheck hiding ((===))
+
+import Text.Printf.TH
+
+newtype Checked a = Checked { getChecked :: a }
+    deriving (Eq,Ord,NFData,Functor,Foldable,Traversable,Typeable)
+
+instance Show a => Show (Checked a) where
+    show (Checked x) = show x
+
+#if MIN_VERSION_transformers(0,5,0)
+instance Eq1 Checked where
+    liftEq f (Checked a) (Checked b) = a `f` b
+#else
+instance Eq1 Checked where
+    eq1 (Checked a) (Checked b) = a == b
+#endif
+
+#if MIN_VERSION_transformers(0,5,0)
+instance Show1 Checked where
+    liftShowsPrec f _ i (Checked a) = f i a
+#else
+instance Show1 Checked where
+    showsPrec1 = showsPrec
+#endif
+
+deriving instance Typeable Compose
+
+newtype InvariantM a = Invariant { runInvariant :: RWS [String] [String] () a }
+    deriving (Functor,Applicative,Monad)
+
+type Invariant = InvariantM ()
+
+class Show a => HasInvariant a where
+    invariant :: a -> Invariant
+    updateCache :: a -> a
+    updateCache = id
+
+class HasInvariant b => IsChecked a b | a -> b where
+    check :: Pre
+          => b -> a
+    check' :: Pre
+           => b -> a
+    content :: Pre
+            => Iso' a b
+
+class IsAssertion a where
+    toInvariant :: a -> Invariant
+    fromBool :: Bool -> a
+
+instance (a ~ ()) => Testable (InvariantM a) where
+    property p = conjoin (map (`counterexample` property False) xs)
+        where
+            xs = invariantResults p
+
+instance IsAssertion Bool where
+    toInvariant b = Invariant $ do
+        p <- ask
+        unless b $ tell [intercalate " - " $ reverse p]
+    fromBool = id
+
+instance (a ~ ()) => IsAssertion (InvariantM a) where
+    toInvariant b = b >> return ()
+    fromBool = toInvariant
+
+instance Monoid a => Monoid (InvariantM a) where
+    mempty = return mempty
+    mappend = liftM2 mappend
+    mconcat = fmap mconcat . sequence
+
+class Controls a b | a -> b where
+    content' :: Getter a b
+    default content' :: a ~ b => Getter a b
+    content' = id
+
+infixl 8 !.
+
+(!.) :: Controls a b => a -> Getting c b c -> c
+(!.) = flip view'
+
+view' :: (Controls a b,MonadReader a m) => Getting c b c -> m c
+view' ln = view $ content'.ln
+
+views' :: (Controls a b,MonadReader a m) 
+       => Getting d b c
+       -> (c -> d)
+       -> m d
+views' ln f = views (content'.ln) f
+
+use' :: (Controls a b,MonadState a m) => Getting c b c -> m c
+use' ln = use $ content'.ln
+
+uses' :: (Controls a b,MonadState a m) 
+      => Getting d b c 
+      -> (c -> d) 
+      -> m d
+uses' ln f = uses (content'.ln) f
+
+instance Controls (Checked a) a where
+    content' = to getChecked
+
+instance (Functor f, Show a, Show1 f, Show1 g, HasInvariant (f (g a))) 
+        => HasInvariant (Compose f g a) where
+    invariant = invariant . getCompose
+    updateCache = _Wrapped' %~ updateCache
+
+instance HasInvariant a => IsChecked (Checked a) a where
+    check    = check' . updateCache
+    check' x = Checked $ checkAssert (invariant x) (show x) x
+        where
+            -- msg = [printf|invariant failure: \n%s|] $ intercalate "\n" p
+            -- p = map fst $ filter (not.snd) $ snd $ execRWS (runInvariant $ invariant x) [] ()
+    content = iso getChecked check
+
+holds :: IsAssertion prop => prop -> Bool
+holds prop = null $ snd $ execRWS (runInvariant $ toInvariant prop) [] ()
+
+checkAssertM :: (IsAssertion a,Monad m,Pre) => a -> String -> m ()
+checkAssertM p msg = checkAssert p msg (return ())
+
+checkAssert :: (IsAssertion a,Pre) => a -> String -> b -> b
+checkAssert prop detail x = providedMessage' ?loc "Invariants" msg (null p) x
+        where
+            msg = [s|assertion failure: \n%s\n%s|] (intercalate "\n" p) (take 1000 detail)
+            p = invariantResults prop
+
+invariantResults :: IsAssertion a => a -> [String]
+invariantResults prop = 
+        map (take 1000) . snd $ execRWS (runInvariant $ toInvariant prop) [] ()
+
+invariantMessage :: IsAssertion a => a -> String
+invariantMessage prop 
+        | null p    = "pass"
+        | otherwise = intercalate "\n" $ "failed" : p
+    where
+        p = invariantResults prop
+
+trading :: (Functor f,Functor f')
+        => Iso (Compose f (Compose g h) x) (Compose f' (Compose g' h') x')
+               (Compose f g (h x)) (Compose f' g' (h' x'))
+trading = iso (_Wrapped %~ fmap getCompose) (_Wrapped %~ fmap Compose)
+
+instance Controls (Compose Checked f a) (f a) where
+    content' = to getCompose . content'
+
+instance HasInvariant (f a) => IsChecked (Compose Checked f a) (f a) where
+    check   = Compose . check
+    check'  = Compose . check'
+    content = iso getCompose Compose . content
+
+instance NFData (f (g x)) => NFData (Compose f g x) where
+    rnf = rnf . getCompose
+
+infixr 0 ##
+
+(##) :: (IsAssertion b, Pre) => String -> b -> Invariant
+(##) tag b = withStack ?loc $ withPrefix tag $ toInvariant b
+
+infix 4 ===
+
+(===) :: (Eq a, Show a) => a -> a -> Invariant
+(===) = relation "/=" (==)
+
+isSubsetOf' :: (Ord a,Show a) => Set a -> Set a -> Invariant
+isSubsetOf' = relation "/⊆" isSubsetOf
+
+isProperSubsetOf' :: (Ord a,Show a) => Set a -> Set a -> Invariant
+isProperSubsetOf' = relation "/⊂" isProperSubsetOf
+
+{-# INLINE isSubmapOf' #-}
+isSubmapOf' :: (Ord k,Eq k,Eq a,Show k,Show a) 
+            => Map k a -> Map k a -> Invariant
+isSubmapOf' = relation "/⊆" isSubmapOf
+
+{-# INLINE isProperSubmapOf' #-}
+isProperSubmapOf' :: (Eq k, Eq a,Ord k,Show k,Show a) 
+                  => Map k a -> Map k a -> Invariant
+isProperSubmapOf' = relation "/⊂" isProperSubmapOf
+
+{-# INLINE member' #-}
+member' :: (Show k,Show a,Ord k) 
+        => k -> Map k a -> Invariant
+member' = relation "/∈" member
+
+relation :: (Show a,Show b) 
+         => String 
+         -> (a -> b -> Bool) 
+         -> a -> b -> Invariant
+relation symb rel x y = [s|%s %s %s|] (show x) symb (show y) ## (x `rel` y)
+
+class HasPrefix m where
+    withPrefix :: String -> m a -> m a
+    
+instance HasPrefix InvariantM where
+    withPrefix pre (Invariant cmd) = Invariant $ local (pre:) cmd
+
+instance (HasInvariant a,Arbitrary a) => Arbitrary (Checked a) where
+    arbitrary = check' <$> arbitrary
+    shrink = fmap check' . shrink . getChecked
+
+mutate :: (IsChecked c a,Pre)
+       => c -> State a k -> c
+mutate x cmd = x & content %~ execState cmd 
+
+mutate' :: (IsChecked c a,Monad m,Pre) => StateT a m k -> StateT c m k
+mutate' = zoom content
+
+create' :: (IsChecked c a,Default a,Pre) => State a k -> c
+create' = check . flip execState def 
+
+withStack :: CallStack -> InvariantM a -> InvariantM a
+withStack cs = maybe id withPrefix $ stackTrace [__FILE__] cs
diff --git a/Control/Precondition.hs b/Control/Precondition.hs
new file mode 100644
--- /dev/null
+++ b/Control/Precondition.hs
@@ -0,0 +1,115 @@
+{-# LANGUAGE RankNTypes
+        , CPP
+        , ImplicitParams
+        , ConstraintKinds #-}
+module Control.Precondition
+    ( module Control.Precondition
+    , module Data.Maybe
+    , module Data.Either.Combinators
+    , Loc(..) )
+where
+
+import Control.Exception
+import Control.Exception.Assert (assertMessage)
+import Control.Lens
+
+import Data.Either.Combinators hiding
+        ( fromRight',fromLeft'
+        , mapLeft,mapRight
+        , mapBoth, isRight, isLeft )
+import Data.List.NonEmpty
+import Data.Maybe hiding (fromJust)
+
+import GHC.Stack.Utils
+
+import Language.Haskell.TH
+import Language.Haskell.TH.Syntax
+
+import Language.Haskell.TH.Lift
+
+import Text.Printf
+
+fromJust' :: Pre => Maybe a -> a
+fromJust' (Just x)   = x
+fromJust' Nothing = assertFalse' "Nothing"
+
+fromRight' :: Pre => Either a b -> b
+fromRight' (Right x) = x
+fromRight' (Left _)  = assertFalse' "Left"
+
+
+fromLeft' :: Pre => Either a b -> a
+fromLeft' (Left x) = x
+fromLeft' (Right _)  = assertFalse' "Right"
+
+
+nonEmpty' :: Pre => [a] -> NonEmpty a
+nonEmpty' (x : xs) = x :| xs
+nonEmpty' []    = assertFalse' "empty list cast as non empty"
+
+(!) :: (Pre, Ixed m)
+    => m -> Index m -> IxValue m
+(!) m x = fromJust' $ m^?ix x
+
+byPred :: (Show x,Pre)
+       => String -> (x -> Bool) -> x -> a -> a
+byPred msg p x = providedMessage' ?loc "byPred" (msg ++ "\n" ++ show x) (p x)
+
+byEq :: (Eq x, Show x,Pre) => String -> x -> x -> a -> a
+byEq msg = byRel' msg (==) "≠"
+
+byOrd :: (Ord x, Show x,Pre) => String -> Ordering -> x -> x -> a -> a
+byOrd msg ord = byRel' msg (\x y -> ord == compare x y) symb
+    where
+        symb = case ord of
+                    LT -> "≮"
+                    GT -> "≯"
+                    EQ -> "≠"
+
+byRel :: (Show a,Pre) => String -> (a -> a -> Bool) -> a -> a -> x -> x
+byRel msg rel = byRel' msg rel "/rel/"
+
+byRel' :: (Show a,Pre) => String -> (a -> a -> Bool) -> String -> a -> a -> x -> x
+byRel' tag rel symb x0 x1 r = providedMessage' ?loc tag
+    (show x0 ++ " " ++ symb ++ " " ++ show x1) (x0 `rel` x1) r
+
+type Pre = (?loc :: CallStack)
+
+
+assertFalse' :: Pre => String -> a
+assertFalse' msg = providedMessage' (?loc) "assertion" msg False (error "false assertion: ")
+
+undefined' :: Pre => a
+undefined' = provided False (error "undefined")
+
+assertFalseMessage :: Pre => String -> a
+assertFalseMessage msg = providedMessage' ?loc "False assert" msg False (error "false assertion (2)")
+
+provided :: Pre => Bool -> a -> a
+provided = provided' ?loc
+
+
+
+
+provided' :: CallStack -> Bool -> a -> a
+provided' cs b = assertMessage "Precondition"
+        (fromMaybe "" $ stackTrace [__FILE__] cs) (assert b)
+
+providedMessage' :: CallStack -> String -> String -> Bool -> a -> a
+providedMessage' cs tag msg b = assertMessage tag
+        (fromMaybe "" (stackTrace [__FILE__] cs) ++ "\n" ++ msg) (assert b)
+
+providedM :: Pre => Bool -> m a -> m a
+providedM b cmd = do
+        provided b () `seq` cmd
+
+locMsg :: Loc -> String
+locMsg loc = printf "%s:%d:%d" (loc_filename loc) (fst $ loc_start loc) (snd $ loc_end loc)
+
+withLoc :: Name -> ExpQ
+withLoc fun = do
+    loc <- location
+    [e| $(varE fun) $(lift loc) |]
+
+instance Lift Loc where
+    lift = $(makeLift ''Loc)
diff --git a/GHC/Stack/Utils.hs b/GHC/Stack/Utils.hs
new file mode 100644
--- /dev/null
+++ b/GHC/Stack/Utils.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE CPP #-}
+module GHC.Stack.Utils
+    ( module GHC.Stack.Utils
+    , module GHC.Stack )
+where
+
+import Data.Maybe
+
+import GHC.Stack
+
+#if !(MIN_VERSION_base(4,9,0))
+import GHC.SrcLoc
+#endif
+
+
+import Text.Printf
+
+stackTrace' :: [FilePath] -> CallStack -> String -> String
+stackTrace' fs stack str = fromMaybe str $ stackTrace fs stack
+
+getSrcLocs :: [FilePath] -> CallStack -> [(String,SrcLoc)]
+getSrcLocs fs cs = filter notHere $ getCallStack cs
+    where
+        notHere :: (a,SrcLoc) -> Bool
+        notHere (_,x) = srcLocFile x `notElem` __FILE__:fs
+
+stackTrace :: [FilePath] -> CallStack -> Maybe String
+stackTrace fs cs | null loc  = Nothing
+                 | otherwise = Just $ '\n':concatMap f (reverse loc)
+    where
+        loc = getSrcLocs fs cs
+        f (fn,loc) = printf "%s - %s\n" (locToString loc) fn
+
+locToString :: SrcLoc -> String
+locToString loc = printf "%s:%d:%d" 
+            (srcLocFile loc) 
+            (srcLocStartLine loc)
+            (srcLocStartCol loc)
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2016 Simon Hudon
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
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/control-invariants.cabal b/control-invariants.cabal
new file mode 100644
--- /dev/null
+++ b/control-invariants.cabal
@@ -0,0 +1,79 @@
+-- Initial invariants.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+-- The name of the package.
+name:                control-invariants
+
+-- The package version.  See the Haskell package versioning policy (PVP) 
+-- for standards guiding when and how versions should be incremented.
+-- http://www.haskell.org/haskellwiki/Package_versioning_policy
+-- PVP summary:      +-+------- breaking API changes
+--                   | | +----- non-breaking API additions
+--                   | | | +--- code changes with no API change
+version:             0.1.0.0
+
+-- A short (one-line) description of the package.
+synopsis:            Invariants and contract monitoring
+
+-- A longer description of the package.
+description:         Invariants and contract monitoring
+
+-- The license under which the package is released.
+license:             MIT
+
+-- The file containing the license text.
+license-file:        LICENSE
+
+-- The package author(s).
+author:              Simon Hudon
+
+-- An email address to which users can send suggestions, bug reports, and 
+-- patches.
+maintainer:          simon@cse.yorku.ca
+
+-- A copyright notice.
+-- copyright:           
+
+category:            Control
+
+build-type:          Simple
+
+-- Extra files to be distributed with the package, such as examples or a 
+-- README.
+-- extra-source-files:  
+
+-- Constraint on the version of Cabal needed to build this package.
+cabal-version:       >=1.10
+
+source-repository head
+  type: git
+  location: https://github.com/literate-unitb/invariants.git
+
+library
+  -- Modules exported by the library.
+  exposed-modules:     
+      Control.Invariant
+      Control.Precondition
+      GHC.Stack.Utils
+  
+  -- Modules included in this library but not exported.
+  -- other-modules:       
+  
+  -- LANGUAGE extensions used by modules in this package.
+  default-extensions:    StandaloneDeriving, TypeFamilies, RankNTypes, TemplateHaskell, ImplicitParams, ConstraintKinds, QuasiQuotes, DefaultSignatures, MultiParamTypeClasses, FunctionalDependencies, GeneralizedNewtypeDeriving, DeriveFunctor, DeriveFoldable, DeriveTraversable
+  
+  -- Other library packages from which modules are imported.
+  build-depends:       base >=4.8 && <5, deepseq >=1.4 && <1.5, lens >=4.12 && <4.15, mtl >=2.2 && <2.3, data-default >=0.5 && <0.8, transformers >=0.4 && <0.6, containers >=0.5 && <0.6, assert >=0.0 && <0.1, either >=4.4 && <4.5, semigroups >=0.16 && <0.19, template-haskell >=2.10 && <2.12, th-lift, th-printf, QuickCheck
+  
+  ghc-options: -W -fwarn-missing-signatures 
+         -fwarn-incomplete-uni-patterns
+         -fwarn-missing-methods
+         -fno-ignore-asserts
+         -fwarn-tabs
+         -j8
+
+  -- Directories containing source files.
+  hs-source-dirs:      .
+  
+  -- Base language which the package is written in.
+  default-language:    Haskell2010