diff --git a/hardhat.modelcheck.config.js b/hardhat.modelcheck.config.js
new file mode 100644
index 0000000..09b7d0f
--- /dev/null
+++ b/hardhat.modelcheck.config.js
@@ -0,0 +1,11 @@
+const config = require("./hardhat.config")
+
+config.solidity.settings.modelChecker = {
+  engine: "chc",
+  showUnproved: true,
+  contracts: {
+    "contracts/TestCollateral.sol": ["TestCollateral"],
+  },
+}
+
+module.exports = config
diff --git a/package.json b/package.json
index 99abdfb..42a5b01 100644
--- a/package.json
+++ b/package.json
@@ -5,7 +5,8 @@
     "test": "npm run lint && hardhat test",
     "start": "hardhat node --export deployment-localhost.json",
     "format": "prettier --write contracts/**/*.sol test/**/*.js",
-    "lint": "solhint contracts/**.sol"
+    "lint": "solhint contracts/**.sol",
+    "modelcheck": "hardhat compile --config hardhat.modelcheck.config.js --force"
   },
   "devDependencies": {
     "@nomiclabs/hardhat-ethers": "^2.2.1",