diff --git a/pkgs/development/python-modules/model-checker/default.nix b/pkgs/development/python-modules/model-checker/default.nix
new file mode 100644
index 000000000000..685282decd33
--- /dev/null
+++ b/pkgs/development/python-modules/model-checker/default.nix
@@ -0,0 +1,45 @@
+{
+  lib,
+  buildPythonPackage,
+  fetchPypi,
+  setuptools,
+  pythonOlder,
+  z3-solver,
+  pythonRelaxDepsHook,
+}:
+
+buildPythonPackage rec {
+  pname = "model-checker";
+  version = "0.3.13";
+  pyproject = true;
+
+  disabled = pythonOlder "3.8";
+
+  src = fetchPypi {
+    pname = "model_checker";
+    inherit version;
+    hash = "sha256-3LVes+orRl8tNhhbUUDa1VM/tFf8Y1pAzKknmrjA6e4=";
+  };
+
+  # z3 does not provide a dist-info, so python-runtime-deps-check will fail
+  pythonRemoveDeps = [ "z3-solver" ];
+
+  build-system = [ setuptools ];
+
+  nativeBuildInputs = [ pythonRelaxDepsHook ];
+
+  dependencies = [ z3-solver ];
+
+  # Tests have multiple issues, ImportError, TypeError, etc.
+  # Check with the next release > 0.3.13
+  doCheck = false;
+
+  pythonImportsCheck = [ "model_checker" ];
+
+  meta = with lib; {
+    description = "A hyperintensional theorem prover for counterfactual conditionals and modal operators";
+    homepage = "https://pypi.org/project/model-checker/";
+    license = licenses.mit;
+    maintainers = with maintainers; [ fab ];
+  };
+}
diff --git a/pkgs/top-level/python-packages.nix b/pkgs/top-level/python-packages.nix
index ab5b1f6e9ed5..73bf650c68c3 100644
--- a/pkgs/top-level/python-packages.nix
+++ b/pkgs/top-level/python-packages.nix
@@ -7616,6 +7616,8 @@ self: super: with self; {
 
   model-bakery = callPackage ../development/python-modules/model-bakery { };
 
+  model-checker = callPackage ../development/python-modules/model-checker { };
+
   modelcif = callPackage ../development/python-modules/modelcif { };
 
   modeled = callPackage ../development/python-modules/modeled { };