diff --git a/released/packages/coq-vst-zlist/coq-vst-zlist.2.12/opam b/released/packages/coq-vst-zlist/coq-vst-zlist.2.12/opam
new file mode 100644
index 0000000000..e10b0ee99c
--- /dev/null
+++ b/released/packages/coq-vst-zlist/coq-vst-zlist.2.12/opam
@@ -0,0 +1,24 @@
+opam-version: "2.0"
+synopsis: "A list library indexed by Z type, with a powerful automatic solver"
+authors: [
+  "Qinshi Wang"
+  "Andrew W. Appel"
+]
+maintainer: "VST team"
+homepage: "http://vst.cs.princeton.edu/"
+dev-repo: "git+https://github.com/PrincetonUniversity/VST.git"
+bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
+license: "BSD-2-Clause"
+
+build: [
+  [make "-C" "zlist" "-j%{jobs}%"]
+]
+run-test: []
+install: [make "-C" "zlist" "install"]
+depends: [
+  "coq" {>= "8.13"}
+]
+url {
+  src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.12.tar.gz"
+  checksum: "sha512=7ca3bf55a7e5888dbfd271d9955c463d00de0e7125c60a45ca568d7de2a75104f0e740ba002e10ce7fd1ab94761c0b876816ffac4ac3f2c49af187891be604b5"
+}
diff --git a/released/packages/coq-vst/coq-vst.2.12/opam b/released/packages/coq-vst/coq-vst.2.12/opam
new file mode 100644
index 0000000000..e247e525b0
--- /dev/null
+++ b/released/packages/coq-vst/coq-vst.2.12/opam
@@ -0,0 +1,50 @@
+opam-version: "2.0"
+synopsis: "Verified Software Toolchain"
+description: "The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context."
+authors: [
+  "Andrew W. Appel"
+  "Lennart Beringer"
+  "Josiah Dodds"
+  "Qinxiang Cao"
+  "Aquinas Hobor"
+  "Gordon Stewart"
+  "Qinshi Wang"
+  "Sandrine Blazy"
+  "Santiago Cuellar"
+  "Robert Dockins"
+  "Nick Giannarakis"
+  "Samuel Gruetter"
+  "Jean-Marie Madiot"
+]
+maintainer: "VST team"
+homepage: "http://vst.cs.princeton.edu/"
+dev-repo: "git+https://github.com/PrincetonUniversity/VST.git"
+bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
+license: "BSD-2-Clause"
+
+build: [
+  [make "-j%{jobs}%" "vst" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
+]
+install: [
+  [make "install" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
+]
+run-test: [
+  [make "-j%{jobs}%" "test" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
+]
+depends: [
+  "ocaml"
+  "coq" {>= "8.14" & < "8.18~"}
+  "coq-compcert" {= "3.12"}
+  "coq-vst-zlist" {= version}
+  "coq-flocq" {>= "4.1.0"}
+]
+tags: [
+  "category:Computer Science/Semantics and Compilation/Semantics"
+  "keyword:C"
+  "logpath:VST"
+  "date:2023-03-31"
+]
+url {
+  src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.12.tar.gz"
+  checksum: "sha512=7ca3bf55a7e5888dbfd271d9955c463d00de0e7125c60a45ca568d7de2a75104f0e740ba002e10ce7fd1ab94761c0b876816ffac4ac3f2c49af187891be604b5"
+}