diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,17 @@
+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,6 @@
+module Main(main)
+
+import Distribution.Simple
+
+main :: IO ()
+main = defaultMain
diff --git a/opentheory-primitive.cabal b/opentheory-primitive.cabal
new file mode 100644
--- /dev/null
+++ b/opentheory-primitive.cabal
@@ -0,0 +1,43 @@
+Name: opentheory-primitive
+Version: 1.0
+Category: Formal Methods
+Synopsis: Haskell primitives used by OpenTheory packages
+License: MIT
+License-file: LICENSE
+Cabal-version: >= 1.8.0.6
+Build-type: Simple
+Author: Joe Hurd <joe@gilith.com>
+Maintainer: Joe Hurd <joe@gilith.com>
+Description:
+  The types and values defined in this package extend those in the
+  Prelude to provide the core execution platform assumed by Haskell
+  packages exported from formally verified OpenTheory packages.
+
+Library
+  Build-depends:
+    base >= 4.0 && < 5.0,
+    random >= 1.0.1.1 && < 2.0,
+    QuickCheck >= 2.4.0.1 && < 3.0
+
+  hs-source-dirs: src
+
+  ghc-options: -Wall
+
+  Exposed-modules:
+    OpenTheory.Primitive.Byte
+    OpenTheory.Primitive.Natural
+    OpenTheory.Primitive.Random
+    OpenTheory.Primitive.Word16
+    OpenTheory.Primitive.Test
+
+Executable opentheory-primitive-test
+  Build-depends:
+    base >= 4.0 && < 5.0,
+    random >= 1.0.1.1 && < 2,
+    QuickCheck >= 2.4.0.1 && < 3.0
+
+  hs-source-dirs: src, testsrc
+
+  ghc-options: -Wall
+
+  Main-is: Test.hs
diff --git a/src/OpenTheory/Primitive/Byte.hs b/src/OpenTheory/Primitive/Byte.hs
new file mode 100644
--- /dev/null
+++ b/src/OpenTheory/Primitive/Byte.hs
@@ -0,0 +1,51 @@
+{- |
+Module: $Header$
+Description: Byte primitive functions
+License: MIT
+
+Maintainer: Joe Hurd <joe@gilith.com>
+Stability: provisional
+Portability: portable
+
+Byte primitive functions
+-}
+module OpenTheory.Primitive.Byte
+  ( Byte,
+    and,
+    bit,
+    fromNatural,
+    not,
+    or,
+    shiftLeft,
+    shiftRight )
+where
+
+import Prelude (Bool, (<), (&&), fromIntegral)
+import qualified Data.Bits
+import qualified Data.Word
+import qualified OpenTheory.Primitive.Natural as Primitive.Natural
+
+type Byte = Data.Word.Word8
+
+and :: Byte -> Byte -> Byte
+and w1 w2 = (Data.Bits..&.) w1 w2
+
+bit :: Byte -> Primitive.Natural.Natural -> Bool
+bit w i = i < 8 && Data.Bits.testBit w (fromIntegral i)
+
+fromNatural :: Primitive.Natural.Natural -> Byte
+fromNatural = fromIntegral
+
+not :: Byte -> Byte
+not w = (Data.Bits.complement) w
+
+or :: Byte -> Byte -> Byte
+or w1 w2 = (Data.Bits..|.) w1 w2
+
+shiftLeft :: Byte -> Primitive.Natural.Natural -> Byte
+shiftLeft w n =
+    if n < 8 then (Data.Bits.shiftL) w (fromIntegral n) else 0
+
+shiftRight :: Byte -> Primitive.Natural.Natural -> Byte
+shiftRight w n =
+    if n < 8 then (Data.Bits.shiftR) w (fromIntegral n) else 0
diff --git a/src/OpenTheory/Primitive/Natural.hs b/src/OpenTheory/Primitive/Natural.hs
new file mode 100644
--- /dev/null
+++ b/src/OpenTheory/Primitive/Natural.hs
@@ -0,0 +1,71 @@
+{- |
+Module: $Header$
+Description: A natural number type
+License: MIT
+
+Maintainer: Joe Hurd <joe@gilith.com>
+Stability: provisional
+Portability: portable
+
+A natural number type
+-}
+module OpenTheory.Primitive.Natural
+  ( Natural )
+where
+
+newtype Natural =
+    Natural { unNatural :: Integer }
+  deriving Eq
+
+instance Show Natural where
+  show n = show (unNatural n)
+
+instance Ord Natural where
+  compare x y = compare (unNatural x) (unNatural y)
+
+instance Num Natural where
+  x + y = Natural (unNatural x + unNatural y)
+
+  x - y =
+      if x < y
+        then error "OpenTheory.Primitive.Natural.-"
+        else Natural (unNatural x - unNatural y)
+
+  x * y = Natural (unNatural x * unNatural y)
+
+  abs x = x
+
+  signum x = if unNatural x == 0 then x else Natural 1
+
+  fromInteger x =
+      if x < 0
+        then error "OpenTheory.Primitive.Natural.fromInteger"
+        else Natural x
+
+instance Real Natural where
+  toRational x = toRational (unNatural x)
+
+instance Enum Natural where
+  toEnum x =
+      if x < 0
+        then error "OpenTheory.Primitive.Natural.toEnum"
+        else Natural (toEnum x)
+
+  fromEnum x = fromEnum (unNatural x)
+
+instance Integral Natural where
+  divMod x y =
+      if y == 0
+        then error "OpenTheory.Primitive.Natural.divMod"
+        else
+          let (d,m) = divMod (unNatural x) (unNatural y)
+          in (Natural d, Natural m)
+
+  quotRem x y =
+      if y == 0
+        then error "OpenTheory.Primitive.Natural.quotRem"
+        else
+          let (q,r) = quotRem (unNatural x) (unNatural y)
+          in (Natural q, Natural r)
+
+  toInteger = unNatural
diff --git a/src/OpenTheory/Primitive/Random.hs b/src/OpenTheory/Primitive/Random.hs
new file mode 100644
--- /dev/null
+++ b/src/OpenTheory/Primitive/Random.hs
@@ -0,0 +1,47 @@
+{- |
+Module: $Header$
+Description: Random stream primitives
+License: MIT
+
+Maintainer: Joe Hurd <joe@gilith.com>
+Stability: provisional
+Portability: portable
+
+Random stream primitives
+-}
+module OpenTheory.Primitive.Random
+  ( Random,
+    bit,
+    split,
+    fromInt )
+where
+
+import qualified System.Random
+import qualified Test.QuickCheck
+
+data Random =
+    Random
+      { seed :: Int,
+        gen :: System.Random.StdGen }
+
+instance Test.QuickCheck.Arbitrary Random where
+  arbitrary = fmap fromInt Test.QuickCheck.arbitrary
+
+instance Show Random where
+  show r = "Random<" ++ show (seed r) ++ ">"
+
+bit :: Random -> (Bool,Random)
+bit r =
+  let (b,g) = System.Random.random (gen r) in
+  (b, r {gen = g})
+
+split :: Random -> (Random,Random)
+split r =
+  let (g1,g2) = System.Random.split (gen r) in
+  (r {gen = g1}, r {gen = g2})
+
+fromInt :: Int -> Random
+fromInt i =
+    Random
+      {seed = i,
+       gen = System.Random.mkStdGen i}
diff --git a/src/OpenTheory/Primitive/Test.hs b/src/OpenTheory/Primitive/Test.hs
new file mode 100644
--- /dev/null
+++ b/src/OpenTheory/Primitive/Test.hs
@@ -0,0 +1,24 @@
+{- |
+Module: $Header$
+Description: OpenTheory QuickCheck interface
+License: MIT
+
+Maintainer: Joe Hurd <joe@gilith.com>
+Stability: provisional
+Portability: portable
+
+OpenTheory QuickCheck interface
+-}
+module OpenTheory.Primitive.Test
+  ( check )
+where
+
+import Test.QuickCheck
+
+checkArgs :: Test.QuickCheck.Args
+checkArgs = Test.QuickCheck.stdArgs { maxSuccess = 100 }
+
+check :: Testable prop => String -> prop -> IO ()
+check desc prop =
+  do putStr desc
+     Test.QuickCheck.quickCheckWith checkArgs prop
diff --git a/src/OpenTheory/Primitive/Word16.hs b/src/OpenTheory/Primitive/Word16.hs
new file mode 100644
--- /dev/null
+++ b/src/OpenTheory/Primitive/Word16.hs
@@ -0,0 +1,60 @@
+{- |
+Module: $Header$
+Description: Word16 primitive functions
+License: MIT
+
+Maintainer: Joe Hurd <joe@gilith.com>
+Stability: provisional
+Portability: portable
+
+Word16 primitive functions
+-}
+module OpenTheory.Primitive.Word16
+  ( Word16,
+    and,
+    bit,
+    fromBytes,
+    fromNatural,
+    not,
+    or,
+    shiftLeft,
+    shiftRight,
+    toBytes )
+where
+
+import Prelude (Bool, (<), (&&), fromIntegral)
+import qualified Data.Bits
+import qualified Data.Word
+import qualified OpenTheory.Primitive.Byte as Primitive.Byte
+import qualified OpenTheory.Primitive.Natural as Primitive.Natural
+
+type Word16 = Data.Word.Word16
+
+and :: Word16 -> Word16 -> Word16
+and w1 w2 = (Data.Bits..&.) w1 w2
+
+bit :: Word16 -> Primitive.Natural.Natural -> Bool
+bit w i = i < 16 && Data.Bits.testBit w (fromIntegral i)
+
+fromBytes :: Primitive.Byte.Byte -> Primitive.Byte.Byte -> Word16
+fromBytes b0 b1 = or (fromIntegral b0) (shiftLeft (fromIntegral b1) 8)
+
+fromNatural :: Primitive.Natural.Natural -> Word16
+fromNatural = fromIntegral
+
+not :: Word16 -> Word16
+not w = (Data.Bits.complement) w
+
+or :: Word16 -> Word16 -> Word16
+or w1 w2 = (Data.Bits..|.) w1 w2
+
+shiftLeft :: Word16 -> Primitive.Natural.Natural -> Word16
+shiftLeft w n =
+    if n < 16 then (Data.Bits.shiftL) w (fromIntegral n) else 0
+
+shiftRight :: Word16 -> Primitive.Natural.Natural -> Word16
+shiftRight w n =
+    if n < 16 then (Data.Bits.shiftR) w (fromIntegral n) else 0
+
+toBytes :: Word16 -> (Primitive.Byte.Byte,Primitive.Byte.Byte)
+toBytes w = (fromIntegral w, fromIntegral (shiftRight w 8))
diff --git a/testsrc/Test.hs b/testsrc/Test.hs
new file mode 100644
--- /dev/null
+++ b/testsrc/Test.hs
@@ -0,0 +1,27 @@
+{- |
+Module: $Header$
+Description: OpenTheory QuickCheck interface
+License: MIT
+
+Maintainer: Joe Hurd <joe@gilith.com>
+Stability: provisional
+Portability: portable
+
+OpenTheory QuickCheck interface
+-}
+module Main
+  ( main )
+where
+
+import qualified OpenTheory.Primitive.Random as Primitive.Random
+import qualified OpenTheory.Primitive.Test as Primitive.Test
+
+proposition0 :: Primitive.Random.Random -> Bool
+proposition0 r =
+  let (p,_) = Primitive.Random.bit r in
+  p || not p
+
+main :: IO ()
+main =
+    do Primitive.Test.check "Proposition 0:\n  !p. p \\/ ~p\n  " proposition0
+       return ()