diff --git a/hcc.cabal b/hcc.cabal
index d898484..ef0a7f6 100644
--- a/hcc.cabal
+++ b/hcc.cabal
@@ -12,7 +12,7 @@ homepage:           github.com/danr/contracts
 executable          hcc
     ghc-options:    -O2 -package ghc -Wall -auto-all
     hs-source-dirs: src halo/src
-    main-is:        Main.hs
+    main-is:        Contracts/Main.hs
 
     build-depends:
         -- Shared
diff --git a/src/Main.hs b/src/Contracts/Main.hs
similarity index 99%
rename from src/Main.hs
rename to src/Contracts/Main.hs
index a43dd73..f2ca7a9 100644
--- a/src/Main.hs
+++ b/src/Contracts/Main.hs
@@ -89,7 +89,7 @@ import Halo.Subtheory
 import Halo.Trim
 import Halo.Util
 
-import Models.Pipe
+import Contracts.Models.Pipe
 
 import Contracts.Axioms
 import Contracts.Collect
diff --git a/src/Models/Model.hs b/src/Contracts/Models/Model.hs
similarity index 97%
rename from src/Models/Model.hs
rename to src/Contracts/Models/Model.hs
index e6decb6..53c4e9c 100644
--- a/src/Models/Model.hs
+++ b/src/Contracts/Models/Model.hs
@@ -4,7 +4,7 @@
     A prover-agnostic representation of the different components of a model
 
 -}
-module Models.Model where
+module Contracts.Models.Model where
 
 -- | We call everything that is deemed a function in FOL a Symbol here
 data Symbol
diff --git a/src/Models/ParadoxParser.hs b/src/Contracts/Models/ParadoxParser.hs
similarity index 98%
rename from src/Models/ParadoxParser.hs
rename to src/Contracts/Models/ParadoxParser.hs
index b90d93a..18d9c33 100644
--- a/src/Models/ParadoxParser.hs
+++ b/src/Contracts/Models/ParadoxParser.hs
@@ -110,7 +110,7 @@ p_1_Cons(!4) = !1
 +++ END MODEL
 
 -}
-module Models.ParadoxParser (parseParadoxModel) where
+module Contracts.Models.ParadoxParser (parseParadoxModel) where
 
 import Control.Arrow
 
@@ -119,7 +119,7 @@ import Data.List
 import Data.List.Split -- split
 
 
-import Models.Model
+import Contracts.Models.Model
 
 parseParadoxModel :: String -> Model
 parseParadoxModel xs = Model
diff --git a/src/Models/Pipe.hs b/src/Contracts/Models/Pipe.hs
similarity index 94%
rename from src/Models/Pipe.hs
rename to src/Contracts/Models/Pipe.hs
index 21f287b..0a0963a 100644
--- a/src/Models/Pipe.hs
+++ b/src/Contracts/Models/Pipe.hs
@@ -4,13 +4,13 @@
     "Pipe" a problem to paradox with some timeout and print the result
 
 -}
-module Models.Pipe where
+module Contracts.Models.Pipe where
 
 import Type
 
-import Models.Show
-import Models.TypeType ()
-import Models.ParadoxParser
+import Contracts.Models.Show
+import Contracts.Models.TypeType ()
+import Contracts.Models.ParadoxParser
 
 import Contracts.Params
 
diff --git a/src/Models/ProtoType.hs b/src/Contracts/Models/ProtoType.hs
similarity index 95%
rename from src/Models/ProtoType.hs
rename to src/Contracts/Models/ProtoType.hs
index e100be1..3182bea 100644
--- a/src/Models/ProtoType.hs
+++ b/src/Contracts/Models/ProtoType.hs
@@ -3,10 +3,10 @@
     A prototype type, for debugging
 
 -}
-module Models.ProtoType where
+module Contracts.Models.ProtoType where
 
-import Models.Show (Typelike(..))
-import Models.Model
+import Contracts.Models.Show (Typelike(..))
+import Contracts.Models.Model
 
 import Data.Maybe
 import Control.Arrow (first)
diff --git a/src/Models/Show.hs b/src/Contracts/Models/Show.hs
similarity index 99%
rename from src/Models/Show.hs
rename to src/Contracts/Models/Show.hs
index d426611..887ca66 100644
--- a/src/Models/Show.hs
+++ b/src/Contracts/Models/Show.hs
@@ -154,10 +154,10 @@ the function is not min, then don't write this case)
 
 
 -}
-module Models.Show where
+module Contracts.Models.Show where
 
-import Models.Model
-import Models.Spin
+import Contracts.Models.Model
+import Contracts.Models.Spin
 
 
 import qualified Data.Map as M
diff --git a/src/Models/Spin.hs b/src/Contracts/Models/Spin.hs
similarity index 94%
rename from src/Models/Spin.hs
rename to src/Contracts/Models/Spin.hs
index 4568ca2..521e9d1 100644
--- a/src/Models/Spin.hs
+++ b/src/Contracts/Models/Spin.hs
@@ -10,12 +10,12 @@
     memo it with a Map over the domain.
 
 -}
-module Models.Spin where
+module Contracts.Models.Spin where
 
 import Control.Monad
 import Control.Applicative
 
-import Models.Model
+import Contracts.Models.Model
 
 -- | Gives the domain of a given size
 domain :: DomSize -> [Elt]
diff --git a/src/Models/Test.hs b/src/Contracts/Models/Test.hs
similarity index 82%
rename from src/Models/Test.hs
rename to src/Contracts/Models/Test.hs
index 3ae4276..0113b50 100644
--- a/src/Models/Test.hs
+++ b/src/Contracts/Models/Test.hs
@@ -4,12 +4,12 @@
     ProtoType instance for Typelike.
 
 -}
-module Models.Test where
+module Contracts.Models.Test where
 
-import Models.Model
-import Models.Show
-import Models.ProtoType
-import Models.ParadoxParser
+import Contracts.Models.Model
+import Contracts.Models.Show
+import Contracts.Models.ProtoType
+import Contracts.Models.ParadoxParser
 
 import System.Environment
 
diff --git a/src/Models/TypeTest.hs b/src/Contracts/Models/TypeTest.hs
similarity index 100%
rename from src/Models/TypeTest.hs
rename to src/Contracts/Models/TypeTest.hs
diff --git a/src/Models/TypeType.hs b/src/Contracts/Models/TypeType.hs
similarity index 91%
rename from src/Models/TypeType.hs
rename to src/Contracts/Models/TypeType.hs
index 5f2be77..8fb6de7 100644
--- a/src/Models/TypeType.hs
+++ b/src/Contracts/Models/TypeType.hs
@@ -5,15 +5,15 @@
     The Typelike instance for GHC's Type.
 
 -}
-module Models.TypeType where
+module Contracts.Models.TypeType where
 
 import Type
 import Unify
 import Outputable
 import TysPrim
 
-import Models.Show (Typelike(..))
-import Models.Model
+import Contracts.Models.Show (Typelike(..))
+import Contracts.Models.Model
 
 import Halo.Shared
 
diff --git a/src/Models/Z3Parser.hs b/src/Contracts/Models/Z3Parser.hs
similarity index 100%
rename from src/Models/Z3Parser.hs
rename to src/Contracts/Models/Z3Parser.hs