4 files changed, 67 insertions, 0 deletions
diff --git a/sci-mathematics/Manifest.gz b/sci-mathematics/Manifest.gz
index db98fde7b677..b0c591fbf623 100644
--- a/sci-mathematics/Manifest.gz
+++ b/sci-mathematics/Manifest.gz
diff --git a/sci-mathematics/kind2/Manifest b/sci-mathematics/kind2/Manifest
new file mode 100644
index 000000000000..9fd5569b6195
--- /dev/null
+++ b/sci-mathematics/kind2/Manifest
@@ -0,0 +1,3 @@
+DIST kind2-1.9.0.tar.gz 2009655 BLAKE2B 531e019cd9cd6edf5799b4283c56eda677dd16e6feec5ab8047d30cf5399a94789b0fd9b39e1fc83a1794a9cf496657d7a3c5eb156a9d4c8358e8a00057504f3 SHA512 c2b441aed01e1e95ddc0ad59b0097d58b4c90a1cf04adcc3ec27d1383937dddac1999825eb3d02f81e3f9f4d146c8b5f2e9f2b315317b0566f91867bbb3e528a
+EBUILD kind2-1.9.0.ebuild 726 BLAKE2B 70c115a896bc9c66edf78d79dc1de08c262516bf0a49e260a0431ce04fc0b4e15d3a0d6030b71954bf107ae5e55ada3f84a9e8fbe0d73906688290b0694dffc6 SHA512 9bda054ef98ffdc70555970106770b80b94d074b31c4cda66d558f4328443cabedc237c9ab0bf02869858dbaa799cf13776123c8fa6db506d8237c6f95d68166
+MISC metadata.xml 1209 BLAKE2B 68ee7ebc3767dba25908216711b465461cb41d8bca0e411c8300d43f69cc640ec93cbd8f96100452165bab9f3686ae69bc79c7ea3d3dc07b4a04f7e56e9f61f1 SHA512 11aa943d439bc65838c00438099844990604f9e87dff6804c4a9ad60fc36a9d64495bd1f5c3f8ca2e403d07b218d192a5ec5f73af189c45ade99657e44a9bad9
diff --git a/sci-mathematics/kind2/kind2-1.9.0.ebuild b/sci-mathematics/kind2/kind2-1.9.0.ebuild
new file mode 100644
index 000000000000..012c60845bd5
--- /dev/null
+++ b/sci-mathematics/kind2/kind2-1.9.0.ebuild
@@ -0,0 +1,36 @@
+# Copyright 1999-2023 Gentoo Authors
+# Distributed under the terms of the GNU General Public License v2
+
+EAPI=8
+
+inherit dune
+
+DESCRIPTION="Multi-engine SMT-based automatic model checker"
+HOMEPAGE="https://kind2-mc.github.io/kind2/
+	https://github.com/kind2-mc/kind2/"
+
+if [[ ${PV} == *9999* ]] ; then
+	inherit git-r3
+	EGIT_REPO_URI="https://github.com/kind2-mc/${PN}.git"
+else
+	SRC_URI="https://github.com/kind2-mc/${PN}/archive/v${PV}.tar.gz
+		-> ${P}.tar.gz"
+	KEYWORDS="~amd64"
+fi
+
+LICENSE="Apache-2.0"
+SLOT="0/${PV}"
+IUSE="+ocamlopt test"
+RESTRICT="!test? ( test )"
+
+RDEPEND="
+	dev-ml/menhir:=
+	dev-ml/num:=
+	dev-ml/yojson:=
+	dev-ml/zmq:=
+"
+DEPEND="${RDEPEND}"
+BDEPEND="
+	dev-ml/dune-build-info
+	test? ( dev-ml/ounit2 )
+"
diff --git a/sci-mathematics/kind2/metadata.xml b/sci-mathematics/kind2/metadata.xml
new file mode 100644
index 000000000000..faf6e30c3a71
--- /dev/null
+++ b/sci-mathematics/kind2/metadata.xml
@@ -0,0 +1,28 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <maintainer type="project">
+    <email>ml@gentoo.org</email>
+    <name>ML</name>
+  </maintainer>
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</email>
+    <name>Gentoo Mathematics Project</name>
+  </maintainer>
+  <longdescription>
+    Kind 2 is an open-source, multi-engine, SMT-based automatic model checker
+    for safety properties of finite-state or infinite-state synchronous
+    reactive systems expressed as in an extension of the Lustre language. In
+    its basic configuration it takes as input one or more Lustre files
+    annotated with properties to be proven invariant, and outputs for each
+    property either a confirmation or a counterexample, i.e., a sequence inputs
+    that falsifies the property. More advanced features include contract-based
+    compositional verification, proof generation for proven properties, and
+    contract-based test generation.
+  </longdescription>
+  <upstream>
+    <bugs-to>https://github.com/kind2-mc/kind2/issues/</bugs-to>
+    <remote-id type="github">kind2-mc/kind2</remote-id>
+  </upstream>
+</pkgmetadata>