diff --git a/heifer.opam b/heifer.opam
new file mode 100644
index 0000000..6c6d30a
--- /dev/null
+++ b/heifer.opam
@@ -0,0 +1,38 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Program verifier"
+description: "A verifier for effectful, higher-order OCaml programs"
+maintainer: ["e0210374@u.nus.edu, darius.foo.tw@gmail.com"]
+authors: ["Song Yahui, Darius Foo"]
+license: "MIT"
+homepage: "https://github.com/hipsleek/Heifer"
+bug-reports: "https://github.com/hipsleek/Heifer/issues"
+depends: [
+  "ocaml" {>= "5"}
+  "z3" {>= "4.12.2"}
+  "menhir" {>= "20220210"}
+  "dune" {>= "3.17" & >= "3.8.0"}
+  "ppx_deriving" {>= "5.2.1"}
+  "ppx_expect" {>= "v0.15.1"}
+  "brr" {>= "0.0.4"}
+  "why3-ide" {>= "1.8.0"}
+  "js_of_ocaml" {>= "5.4.0"}
+  "unionFind" {>= "20220122"}
+  "visitors" {>= "20210608"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/hipsleek/Heifer.git"