diff --git a/released/packages/coq-paco/coq-paco.4.2.3/opam b/released/packages/coq-paco/coq-paco.4.2.3/opam
new file mode 100644
index 000000000..405c6af79
--- /dev/null
+++ b/released/packages/coq-paco/coq-paco.4.2.3/opam
@@ -0,0 +1,35 @@
+opam-version: "2.0"
+maintainer: "gil.hur@sf.snu.ac.kr"
+synopsis: "Coq library implementing parameterized coinduction"
+homepage: "https://github.com/snu-sf/paco/"
+dev-repo: "git+https://github.com/snu-sf/paco.git"
+bug-reports: "https://github.com/snu-sf/paco/issues/"
+authors: [
+  "Chung-Kil Hur <gil.hur@sf.snu.ac.kr>"
+  "Georg Neis <neis@mpi-sws.org>"
+  "Derek Dreyer <dreyer@mpi-sws.org>"
+  "Viktor Vafeiadis <viktor@mpi-sws.org>"
+  "Minki Cho <minki.cho@sf.snu.ac.kr>"
+]
+license: "BSD-3-Clause"
+build: [make "-C" "src" "all" "-j%{jobs}%"]
+install: [make "-C" "src" "-f" "Makefile.coq" "install"]
+depends: [
+  "coq" {>= "8.13" & < "9.1~"}
+]
+tags: [
+  "date:2025-01-30"
+
+  "category:Computer Science/Programming Languages/Formal Definitions and Theory"
+  "category:Mathematics/Logic"
+
+  "keyword:co-induction"
+  "keyword:simulation"
+  "keyword:parameterized greatest fixed point"
+
+  "logpath:Paco"
+]
+url {
+  http: "https://github.com/snu-sf/paco/archive/v4.2.3.tar.gz"
+  checksum: "sha512=b757a24b732e0fdbcc08979d99e9fca9b91d4b53ed9fff56e1dd1ef4fd3f45688d9e1cf67356102fd01303120b4f68460a815582122b5ea9ece12ff86048fbab"
+}