diff --git a/coq-sf-lf.opam b/coq-sf-lf.opam
new file mode 100644
index 000000000..671d6460c
--- /dev/null
+++ b/coq-sf-lf.opam
@@ -0,0 +1,36 @@
+opam-version: "2.0"
+homepage: "https://softwarefoundations.cis.upenn.edu/"
+doc: "https://softwarefoundations.cis.upenn.edu/"
+authors: [
+  "Benjamin C. Pierce"
+  "Arthur Azevedo de Amorim"
+  "Chris Casinghino"
+  "Marco Gaboardi"
+  "Michael Greenberg"
+  "Cătălin Hriţcu"
+  "Vilhelm Sjöberg"
+  "Andrew Tolmach"
+  "Brent Yorgey"
+]
+license: "like MIT"
+
+build: [
+  [make "-C" "lf-current" "-j%{jobs}%"]
+]
+
+install: [
+  [make "-C" "lf-current" "install"]
+]
+
+bug-reports: "?"
+depends: [
+  "ocaml"
+  "coq"
+]
+synopsis:
+  "Logical Foundations (Volume 1 of Software Foundations)"
+description:
+  "Logical Foundations is the entry-point to the series, covering functional programming, basic concepts of logic, computer-assisted theorem proving, and Coq."
+url {
+  src: "https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz"
+}
diff --git a/coq-sf-plf.opam b/coq-sf-plf.opam
new file mode 100644
index 000000000..0e961ad0a
--- /dev/null
+++ b/coq-sf-plf.opam
@@ -0,0 +1,36 @@
+opam-version: "2.0"
+homepage: "https://softwarefoundations.cis.upenn.edu/"
+doc: "https://softwarefoundations.cis.upenn.edu/"
+authors: [
+  "Benjamin C. Pierce"
+  "Arthur Azevedo de Amorim"
+  "Chris Casinghino"
+  "Marco Gaboardi"
+  "Michael Greenberg"
+  "Cătălin Hriţcu"
+  "Vilhelm Sjöberg"
+  "Andrew Tolmach"
+  "Brent Yorgey"
+]
+license: "like MIT"
+
+build: [
+  [make "-C" "plf-current" "-j%{jobs}%"]
+]
+
+install: [
+  [make "-C" "plf-current" "install"]
+]
+
+bug-reports: "?"
+depends: [
+  "ocaml"
+  "coq"
+]
+synopsis:
+  "Programming Language Foundations (Volume 2 of Software Foundations)"
+description:
+  "Programming Language Foundations surveys the theory of programming languages, including operational semantics, Hoare logic, and static type systems."
+url {
+  src: "https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz"
+}
diff --git a/coq-sf-qc.opam b/coq-sf-qc.opam
new file mode 100644
index 000000000..31ebbf488
--- /dev/null
+++ b/coq-sf-qc.opam
@@ -0,0 +1,37 @@
+opam-version: "2.0"
+homepage: "https://softwarefoundations.cis.upenn.edu/"
+doc: "https://softwarefoundations.cis.upenn.edu/"
+authors: [
+  "Benjamin C. Pierce"
+  "Arthur Azevedo de Amorim"
+  "Chris Casinghino"
+  "Marco Gaboardi"
+  "Michael Greenberg"
+  "Cătălin Hriţcu"
+  "Vilhelm Sjöberg"
+  "Andrew Tolmach"
+  "Brent Yorgey"
+]
+license: "like MIT"
+
+build: [
+  [make "-C" "qc-current" "-j%{jobs}%"]
+]
+
+install: [
+  [make "-C" "qc-current" "install"]
+]
+
+bug-reports: "?"
+depends: [
+  "ocaml"
+  "coq"
+  "coq-quickchick"
+]
+synopsis:
+  "QuickChick: Property-Based Testing in Coq (Volume 4 of Software Foundations)"
+description:
+  "QuickChick introduces tools for combining randomized property-based testing with formal specification and proof in Coq."
+url {
+  src: "https://www.cis.upenn.edu/~bcpierce/sf/qc-current/qc.tgz"
+}
diff --git a/coq-sf-slf.opam b/coq-sf-slf.opam
new file mode 100644
index 000000000..9762a280a
--- /dev/null
+++ b/coq-sf-slf.opam
@@ -0,0 +1,36 @@
+opam-version: "2.0"
+homepage: "https://softwarefoundations.cis.upenn.edu/"
+doc: "https://softwarefoundations.cis.upenn.edu/"
+authors: [
+  "Benjamin C. Pierce"
+  "Arthur Azevedo de Amorim"
+  "Chris Casinghino"
+  "Marco Gaboardi"
+  "Michael Greenberg"
+  "Cătălin Hriţcu"
+  "Vilhelm Sjöberg"
+  "Andrew Tolmach"
+  "Brent Yorgey"
+]
+license: "like MIT"
+
+build: [
+  [make "-C" "slf-current" "-j%{jobs}%"]
+]
+
+install: [
+  [make "-C" "slf-current" "install"]
+]
+
+bug-reports: "?"
+depends: [
+  "ocaml"
+  "coq"
+]
+synopsis:
+  "Separation Logic Foundations (Volume 6 of Software Foundations)"
+description:
+  "Separation Logic Foundations is an in-depth introduction to separation logic, a practical approach to modular verification of imperative programs."
+url {
+  src: "https://www.cis.upenn.edu/~bcpierce/sf/slf-current/slf.tgz"
+}
diff --git a/coq-sf-vc.opam b/coq-sf-vc.opam
new file mode 100644
index 000000000..af35d35ce
--- /dev/null
+++ b/coq-sf-vc.opam
@@ -0,0 +1,37 @@
+opam-version: "2.0"
+homepage: "https://softwarefoundations.cis.upenn.edu/"
+doc: "https://softwarefoundations.cis.upenn.edu/"
+authors: [
+  "Benjamin C. Pierce"
+  "Arthur Azevedo de Amorim"
+  "Chris Casinghino"
+  "Marco Gaboardi"
+  "Michael Greenberg"
+  "Cătălin Hriţcu"
+  "Vilhelm Sjöberg"
+  "Andrew Tolmach"
+  "Brent Yorgey"
+]
+license: "like MIT"
+
+build: [
+  [make "-C" "vc-current" "-j%{jobs}%"]
+]
+
+install: [
+  [make "-C" "vc-current" "install"]
+]
+
+bug-reports: "?"
+depends: [
+  "ocaml"
+  "coq"
+  "coq-vst"
+]
+synopsis:
+  "Verifiable C (Volume 5 of Software Foundations)"
+description:
+  "Verifiable C is an extended hands-on tutorial on specifying and verifying real-world C programs using the Princeton Verified Software Toolchain."
+url {
+  src: "https://www.cis.upenn.edu/~bcpierce/sf/vc-current/vc.tgz"
+}
diff --git a/coq-sf-vfa.opam b/coq-sf-vfa.opam
new file mode 100644
index 000000000..76a45daa1
--- /dev/null
+++ b/coq-sf-vfa.opam
@@ -0,0 +1,36 @@
+opam-version: "2.0"
+homepage: "https://softwarefoundations.cis.upenn.edu/"
+doc: "https://softwarefoundations.cis.upenn.edu/"
+authors: [
+  "Benjamin C. Pierce"
+  "Arthur Azevedo de Amorim"
+  "Chris Casinghino"
+  "Marco Gaboardi"
+  "Michael Greenberg"
+  "Cătălin Hriţcu"
+  "Vilhelm Sjöberg"
+  "Andrew Tolmach"
+  "Brent Yorgey"
+]
+license: "like MIT"
+
+build: [
+  [make "-C" "vfa-current" "-j%{jobs}%"]
+]
+
+install: [
+  [make "-C" "vfa-current" "install"]
+]
+
+bug-reports: "?"
+depends: [
+  "ocaml"
+  "coq"
+]
+synopsis:
+  "Verified Functional Algorithms (Volume 3 of Software Foundations)"
+description:
+  "Verified Functional Algorithms demonstrates how fundamental data structures can be formally specified and mechanically verified."
+url {
+  src: "https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz"
+}