diff --git a/released/packages/coq-mk-reals-axioms/coq-mk-reals-axioms.1.0.0/opam b/released/packages/coq-mk-reals-axioms/coq-mk-reals-axioms.1.0.0/opam
new file mode 100644
index 000000000..5d7cbdaf3
--- /dev/null
+++ b/released/packages/coq-mk-reals-axioms/coq-mk-reals-axioms.1.0.0/opam
@@ -0,0 +1,48 @@
+
+opam-version: "2.0"
+synopsis: "A Coq formalization of the axiomatic definition of real numbers"
+description: """
+This repository presents a Coq formalization of the axiomatic definition of real numbers,
+guided by the 2nd chapter of Zorich's Mathematical Analysis (Part I, 7th expanded edition) and
+based on the formalization of Morse-Kelley (MK) set theory.
+In this work, the key algebraic properties and the uniqueness of real number structure are verified.
+"""
+
+homepage: "https://github.com/1DGW/coq-mk-reals-axioms"
+dev-repo: "git+https://github.com/1DGW/coq-mk-reals-axioms.git"
+bug-reports: "https://github.com/1DGW/coq-mk-reals-axioms/issues"
+maintainer: "dgw@bupt.edu.cn"
+authors: [
+  "Wensheng Yu"
+  "Dakai Guo"
+  "Si Chen"
+  "Guowei Dou"
+  "Shukun Len"
+]
+license: "LGPL-2.1"
+
+depends: [
+  "coq" {>= "8.13.2" & < "8.21~"}
+]
+
+build: [
+  [make ""]
+]
+install: [
+  [make "install"]
+]
+
+url {
+  src: "https://github.com/1DGW/coq-mk-reals-axioms/archive/refs/tags/v1.0.0.tar.gz"
+  checksum: "sha512=3efd9e87bec6b22d6a919036c1d712501a296c1b8a5e84e4e003449183f01a762d6b41b2df35c779f35f596b76fadd87004e803122a9eaaf75076465ae00a194"
+}
+
+tags: [
+  "keyword:set theory"
+  "keyword:Morse-Kelley"
+  "keyword:MK"
+  "reals"
+  "category:Mathematics/Logic"
+  "date:2024-08-22"
+  "logpath:MKReals"
+]