diff --git a/cerberus-bmc.opam b/cerberus-bmc.opam
index e69de29bb..d8268e689 100644
--- a/cerberus-bmc.opam
+++ b/cerberus-bmc.opam
@@ -0,0 +1,21 @@
+opam-version: "2.0"
+synopsis: "Cerberus-BMC"
+description: "Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C"
+license: "BSD-2-Clause"
+maintainer: ["Kayvan Memarian <kayvan.memarian@cl.cam.ac.uk>"]
+authors: [
+  "Stella Lau"
+  "Jean Pichon-Pharabod"
+  "Victor Gomes"
+  "Kayvan Memarian"
+  "Peter Sewell"
+]
+homepage: "https://www.cl.cam.ac.uk/~pes20/cerberus/"
+bug-reports: "https://github.com/rems-project/cerberus/issues"
+depends: [
+  "cerberus-lib"
+  "angstrom" {>= "0.14.0"}
+  "z3"
+  "cmdliner"
+  "lem"
+]
\ No newline at end of file
diff --git a/cerberus-web.opam b/cerberus-web.opam
index e69de29bb..d185466a1 100644
--- a/cerberus-web.opam
+++ b/cerberus-web.opam
@@ -0,0 +1,20 @@
+opam-version: "2.0"
+synopsis: "Cerberus web application"
+description: "Server and client-side web interface for the Cerberus C semantics"
+license: "BSD-2-Clause"
+maintainer: ["Kayvan Memarian <kayvan.memarian@cl.cam.ac.uk>"]
+authors: [
+  "Victor Gomes"
+  "Kayvan Memarian"
+]
+homepage: "https://www.cl.cam.ac.uk/~pes20/cerberus/"
+bug-reports: "https://github.com/rems-project/cerberus/issues"
+depends: [
+  "cerberus-lib"
+  "fpath" {>= "0.7.3"}
+  "ezgzip" {>= "0.2.3"}
+  "cohttp-lwt-unix" {>= "4.0.0"}
+  "cmdliner"
+  "lwt"
+  "base64"
+]
\ No newline at end of file
diff --git a/cerberus.opam b/cerberus.opam
index 1afd8453d..19fab5b89 100644
--- a/cerberus.opam
+++ b/cerberus.opam
@@ -30,6 +30,7 @@ depends: [
   "lem" {>= "2020-06-03"}
   "menhir" {>= "20211230"}
   "result" {>= "1.5"}
+  "cerberus-lib"
 ]
 build: [
   ["dune" "subst"] {pinned}