diff --git a/released/packages/coq-vst-lib/coq-vst-lib.2.15/opam b/released/packages/coq-vst-lib/coq-vst-lib.2.15/opam
new file mode 100644
index 0000000000..0b382e21ed
--- /dev/null
+++ b/released/packages/coq-vst-lib/coq-vst-lib.2.15/opam
@@ -0,0 +1,46 @@
+opam-version: "2.0"
+synopsis: "VSTlib: VST-verified C library for VST-verified clients"
+description: "These program modules, in the form of Verified Software Units,
+may be linked with client-module code  (at the .c/.o level) and proofs (at the .v level)."
+authors: [
+  "Andrew W. Appel"
+  "William Mansky"
+]
+maintainer: "Andrew W. Appel <appel@princeton.edu>"
+homepage: "https://github.com/PrincetonUniversity/VST/tree/v2.15/lib#readme"
+dev-repo: "git+https://github.com/PrincetonUniversity/VST"
+bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
+license: "BSD-2-Clause"
+
+build: [
+  [ make "-C" "lib" "-j%{jobs}%" "proof-only"]
+]
+install: [
+  [ make "-C" "lib" "install" "INSTALLDIR=%{lib}%/coq/user-contrib/VSTlib"]
+]
+run-test: [
+  [ make "-C" "lib" "-j%{jobs}%" "test-only"]
+]
+depends: [
+  "coq" {>= "8.19" & < "8.21~"}
+  "coq-compcert" {>= "3.15"}
+  "coq-flocq" {>= "4.1.0" & < "5.0"}
+  "coq-vcfloat" {>= "2.2"}
+  "coq-vst" {>= "2.15"}
+]
+url {
+  src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.15.tar.gz"
+  checksum: "sha256=44873919ee077b2ce4eb2b7a83c663d3fd673fd7d89c6fc578c46cf10efb4465"
+}
+
+tags: [
+  "date:2025-01-08"
+  "keyword:VST"
+  "keyword:library"
+  "keyword:malloc"
+  "keyword:threads"
+  "keyword:floating-point arithmetic"
+  "category:Miscellaneous/Coq Extensions"
+  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
+  "logpath:VSTlib"
+  ]
diff --git a/released/packages/coq-vst/coq-vst.2.15/opam b/released/packages/coq-vst/coq-vst.2.15/opam
new file mode 100644
index 0000000000..4804728746
--- /dev/null
+++ b/released/packages/coq-vst/coq-vst.2.15/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.19" & < "8.21~"}
+  "coq-compcert" {= "3.15"}
+  "coq-vst-zlist" {= "2.13"}
+  "coq-flocq" {>= "4.2.0"}
+]
+tags: [
+  "category:Computer Science/Semantics and Compilation/Semantics"
+  "keyword:C"
+  "logpath:VST"
+  "date:2025-01-08"
+]
+url {
+  src: "https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.15.tar.gz"
+  checksum: "sha256=44873919ee077b2ce4eb2b7a83c663d3fd673fd7d89c6fc578c46cf10efb4465"
+}