diff --git a/README.md b/README.md
index 0d5962a..6b1d18b 100644
--- a/README.md
+++ b/README.md
@@ -3,5 +3,5 @@
 This is currently a meta-package for the various TenCert components.
 
 * [SHerLOC](https://github.com/leanprover/SHerLOC)
-* [ANPU](https://github.com/leanprover/ANPU)
+* [NKL](https://github.com/leanprover/NKL)
 * [TensorLib](https://github.com/leanprover/TensorLib)
diff --git a/TenCert.lean b/TenCert.lean
index 7edd3ac..b87f03d 100644
--- a/TenCert.lean
+++ b/TenCert.lean
@@ -2,5 +2,5 @@
 -- Import modules here that should be built as part of the library.
 import TenCert.Basic
 import SHerLOC.Basic
-import ANPU.Basic
+import NKL
 import TensorLib.Basic
diff --git a/lake-manifest.json b/lake-manifest.json
index e08f91b..34179d7 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,18 +5,18 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3e2777320ce9326f0f212acac583ffa864dafe89",
+   "rev": "cf77ce5f5b389a593f6ca0689e5d445010afc056",
    "name": "SHerLOC",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/ANPU.git",
+  {"url": "https://github.com/leanprover/NKL.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e989420b95f2c7c091bdb99459d87fdfdcd90898",
-   "name": "ANPU",
+   "rev": "cfe38f61d0606f1b408e654103fdbcb3db5cf064",
+   "name": "NKL",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8103ee2345c79143153213030ee2ebae7b809fe8",
+   "rev": "d1d385414f665926e3a5f5c7eea3b724ff9d5c91",
    "name": "TensorLib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.lean b/lakefile.lean
index 037123d..eb83159 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -7,8 +7,8 @@ package "TenCert" where
 require SHerLOC from git
   "https://github.com/leanprover/SHerLOC.git" @ "main"
 
-require ANPU from git
-  "https://github.com/leanprover/ANPU.git" @ "main"
+require NKL from git
+  "https://github.com/leanprover/NKL.git" @ "main"
 
 require TensorLib from git
   "https://github.com/leanprover/TensorLib.git" @ "main"
diff --git a/lean-toolchain b/lean-toolchain
index 7f0ea50..a254364 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.13.0-rc4