diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 6bcddffbd78..29d23c7d4a8 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -15,7 +15,7 @@ jobs:
 
 # The dependsOn clauses are:
 #  * Everything depends on the canary jobs (the main jdk21 jobs), except those jobs themselves.
-#  * Anything *_jdk11 or *_jdk17 or *_jdk22 depends on *_jdk21.
+#  * Anything *_jdk11 or *_jdk17 or *_jdk23 depends on *_jdk21.
 ## TODO: Sometimes jdkXX jobs, for a previous non-LTS version (such as jdk20) are a bit gratuitous.
 ## They are placeholders for the next non-LTS version (such as jdk22) when it is released.
 ## Leaving those placeholders will ease the edits to this file.
@@ -29,7 +29,7 @@ jobs:
    - typecheck_part1_jdk21
    - typecheck_part2_jdk21
    - misc_jdk21
-   - misc_jdk22
+   - misc_jdk23
   pool:
     vmImage: 'ubuntu-latest'
   steps:
@@ -72,12 +72,12 @@ jobs:
     fetchDepth: 25
   - bash: ./checker/bin-devel/test-cftests-junit.sh
     displayName: test-cftests-junit.sh
-- job: junit_jdk22
+- job: junit_jdk23
   dependsOn:
    - canary_jobs
   pool:
     vmImage: 'ubuntu-latest'
-  container: mdernst/cf-ubuntu-jdk22:latest
+  container: mdernst/cf-ubuntu-jdk23:latest
   timeoutInMinutes: 70
   steps:
   - checkout: self
@@ -117,12 +117,12 @@ jobs:
     fetchDepth: 25
   - bash: ./checker/bin-devel/test-cftests-nonjunit.sh
     displayName: test-cftests-nonjunit.sh
-- job: nonjunit_jdk22
+- job: nonjunit_jdk23
   dependsOn:
    - canary_jobs
   pool:
     vmImage: 'ubuntu-latest'
-  container: mdernst/cf-ubuntu-jdk22:latest
+  container: mdernst/cf-ubuntu-jdk23:latest
   steps:
   - checkout: self
     fetchDepth: 25
@@ -181,14 +181,14 @@ jobs:
     fetchDepth: 25
   - bash: ./checker/bin-devel/test-cftests-inference-part2.sh
     displayName: test-cftests-inference-part2.sh
-- job: inference_jdk22
+- job: inference_jdk23
   dependsOn:
    - canary_jobs
    - inference_part1_jdk21
    - inference_part2_jdk21
   pool:
     vmImage: 'ubuntu-latest'
-  container: mdernst/cf-ubuntu-jdk22:latest
+  container: mdernst/cf-ubuntu-jdk23:latest
   timeoutInMinutes: 90
   steps:
   - checkout: self
@@ -227,10 +227,10 @@ jobs:
   - bash: ./checker/bin-devel/test-misc.sh
     displayName: test-misc.sh
 # This is a canary job, so it has no `dependsOn`.
-- job: misc_jdk22
+- job: misc_jdk23
   pool:
     vmImage: 'ubuntu-latest'
-  container: mdernst/cf-ubuntu-jdk22-plus:latest
+  container: mdernst/cf-ubuntu-jdk23-plus:latest
   steps:
   - checkout: self
     fetchDepth: 25
@@ -281,14 +281,14 @@ jobs:
     fetchDepth: 1000
   - bash: ./checker/bin-devel/test-typecheck-part2.sh
     displayName: test-typecheck-part2.sh
-- job: typecheck_jdk22
+- job: typecheck_jdk23
   dependsOn:
    - canary_jobs
    - typecheck_part1_jdk21
    - typecheck_part2_jdk21
   pool:
     vmImage: 'ubuntu-latest'
-  container: mdernst/cf-ubuntu-jdk22-plus:latest
+  container: mdernst/cf-ubuntu-jdk23-plus:latest
   steps:
   - checkout: self
     fetchDepth: 1000
@@ -346,14 +346,14 @@ jobs:
     fetchDepth: 25
   - bash: ./checker/bin-devel/test-daikon.sh
     displayName: test-daikon-part2.sh
-- job: daikon_jdk22
+- job: daikon_jdk23
   dependsOn:
    - canary_jobs
    - daikon_part1_jdk21
    - daikon_part2_jdk21
   pool:
     vmImage: 'ubuntu-latest'
-  container: mdernst/cf-ubuntu-jdk22:latest
+  container: mdernst/cf-ubuntu-jdk23:latest
   timeoutInMinutes: 80
   steps:
   - checkout: self
@@ -404,13 +404,13 @@ jobs:
     fetchDepth: 25
   - bash: ./checker/bin-devel/test-guava.sh
     displayName: test-guava.sh
-- job: guava_jdk22
+- job: guava_jdk23
   dependsOn:
    - canary_jobs
    - guava_jdk21
   pool:
     vmImage: 'ubuntu-latest'
-  container: mdernst/cf-ubuntu-jdk22:latest
+  container: mdernst/cf-ubuntu-jdk23:latest
   timeoutInMinutes: 70
   steps:
   - checkout: self
@@ -452,13 +452,13 @@ jobs:
     fetchDepth: 25
   - bash: ./checker/bin-devel/test-plume-lib.sh
     displayName: test-plume-lib.sh
-- job: plume_lib_jdk22
+- job: plume_lib_jdk23
   dependsOn:
    - canary_jobs
    - plume_lib_jdk21
   pool:
     vmImage: 'ubuntu-latest'
-  container: mdernst/cf-ubuntu-jdk22:latest
+  container: mdernst/cf-ubuntu-jdk23:latest
   steps:
   - checkout: self
     fetchDepth: 25
@@ -500,13 +500,13 @@ jobs:
 #     fetchDepth: 25
 #   - bash: ./checker/bin-devel/test-downstream.sh
 #     displayName: test-downstream.sh
-# - job: downstream_jdk22
+# - job: downstream_jdk23
 #   dependsOn:
 #    - canary_jobs
 #    - downstream_jdk21
 #   pool:
 #     vmImage: 'ubuntu-latest'
-#   container: mdernst/cf-ubuntu-jdk22:latest
+#   container: mdernst/cf-ubuntu-jdk23:latest
 #   steps:
 #   - checkout: self
 #     fetchDepth: 25
diff --git a/checker/bin-devel/Dockerfile-README b/checker/bin-devel/Dockerfile-README
index 515b8e5475c..15394a81568 100644
--- a/checker/bin-devel/Dockerfile-README
+++ b/checker/bin-devel/Dockerfile-README
@@ -24,6 +24,7 @@ Create the Docker image:
 DOCKERTESTING=""
 # DOCKERTESTING="-testing"
 alias create_upload_docker_image=' \
+  ( [ -z "$INSIDE_EMACS" ] || (echo "Do not run within Emacs" && false) ) && \
   rm -rf dockerdir && \
   mkdir -p dockerdir && \
   (cd dockerdir && \
@@ -64,12 +65,12 @@ export DPROJECT=cf
 create_upload_docker_image
 
 export OS=ubuntu
-export JDKVER=jdk22
+export JDKVER=jdk23
 export DPROJECT=cf
 create_upload_docker_image
 
 export OS=ubuntu
-export JDKVER=jdk22-plus
+export JDKVER=jdk23-plus
 export DPROJECT=cf
 create_upload_docker_image
 
diff --git a/checker/bin-devel/Dockerfile-ubuntu-jdk22 b/checker/bin-devel/Dockerfile-ubuntu-jdk23
similarity index 95%
rename from checker/bin-devel/Dockerfile-ubuntu-jdk22
rename to checker/bin-devel/Dockerfile-ubuntu-jdk23
index cb8314edad7..0f8c0ef962d 100644
--- a/checker/bin-devel/Dockerfile-ubuntu-jdk22
+++ b/checker/bin-devel/Dockerfile-ubuntu-jdk23
@@ -1,15 +1,15 @@
 # Create a Docker image that is ready to run the main Checker Framework tests,
-# using JDK 22.
+# using JDK 23.
 # (This is OpenJDK, not Oracle JDK.  There are different instructions for
 # installing a LTS release of Java.)
 # To convert this file to use a newer JDK, search (from the top level of the
-# Checker Framework and Annotation Tools repositories) for: (java|jdk).?22\b
+# Checker Framework and Annotation Tools repositories) for: (java|jdk).?23\b
 
 # "ubuntu" is the latest LTS release.  "ubuntu:rolling" is the latest release.
 # See releases at https://hub.docker.com/_/ubuntu for available images.
-# See https://packages.ubuntu.com/search?suite=default&section=all&arch=any&keywords=openjdk-22-jdk&searchon=names
+# See https://packages.ubuntu.com/search?suite=default&section=all&arch=any&keywords=openjdk-23-jdk&searchon=names
 # to see what Ubuntu versions support a particular OpenJDK version.
-FROM ubuntu:mantic
+FROM ubuntu:oracular
 MAINTAINER Michael Ernst <mernst@cs.washington.edu>
 
 # According to
@@ -31,7 +31,7 @@ RUN export DEBIAN_FRONTEND=noninteractive \
   ca-certificates-java \
 && aptitude -y install \
   openjdk-17-jdk \
-  openjdk-22-jdk
+  openjdk-23-jdk
 
 # Known good combinations of JTReg and the JDK appear at https://builds.shipilev.net/jtreg/ .
 
diff --git a/checker/bin-devel/Dockerfile-ubuntu-jdk22-plus b/checker/bin-devel/Dockerfile-ubuntu-jdk23-plus
similarity index 95%
rename from checker/bin-devel/Dockerfile-ubuntu-jdk22-plus
rename to checker/bin-devel/Dockerfile-ubuntu-jdk23-plus
index 3c92f51f90f..e6c7299b828 100644
--- a/checker/bin-devel/Dockerfile-ubuntu-jdk22-plus
+++ b/checker/bin-devel/Dockerfile-ubuntu-jdk23-plus
@@ -1,15 +1,15 @@
 # Create a Docker image that is ready to run the full Checker Framework tests,
-# including building the manual and Javadoc, using JDK 22.
+# including building the manual and Javadoc, using JDK 23.
 # (This is OpenJDK, not Oracle JDK.  There are different instructions for
 # installing a LTS release of Java.)
 # To convert this file to use a newer JDK, search (from the top level of the
-# Checker Framework and Annotation Tools repositories) for: (java|jdk).?22\b
+# Checker Framework and Annotation Tools repositories) for: (java|jdk).?23\b
 
 # "ubuntu" is the latest LTS release.  "ubuntu:rolling" is the latest release.
 # See releases at https://hub.docker.com/_/ubuntu for available images.
-# See https://packages.ubuntu.com/search?suite=default&section=all&arch=any&keywords=openjdk-22-jdk&searchon=names
+# See https://packages.ubuntu.com/search?suite=default&section=all&arch=any&keywords=openjdk-23-jdk&searchon=names
 # to see what Ubuntu versions support a particular OpenJDK version.
-FROM ubuntu:mantic
+FROM ubuntu:oracular
 MAINTAINER Michael Ernst <mernst@cs.washington.edu>
 
 # According to
@@ -31,7 +31,7 @@ RUN export DEBIAN_FRONTEND=noninteractive \
   ca-certificates-java \
 && aptitude -y install \
   openjdk-17-jdk \
-  openjdk-22-jdk
+  openjdk-23-jdk
 
 # Known good combinations of JTReg and the JDK appear at https://builds.shipilev.net/jtreg/ .
 
diff --git a/checker/bin/wpi-many.sh b/checker/bin/wpi-many.sh
index 831f0b0c8b4..10574c77a97 100755
--- a/checker/bin/wpi-many.sh
+++ b/checker/bin/wpi-many.sh
@@ -80,11 +80,11 @@ else
   has_java21="yes"
 fi
 
-# shellcheck disable=SC2153 # testing for JAVA22_HOME, not a typo of JAVA_HOME
-if [ "${JAVA22_HOME}" = "" ]; then
-  has_java22="no"
+# shellcheck disable=SC2153 # testing for JAVA23_HOME, not a typo of JAVA_HOME
+if [ "${JAVA23_HOME}" = "" ]; then
+  has_java23="no"
 else
-  has_java22="yes"
+  has_java23="yes"
 fi
 
 if [ "${has_java_home}" = "yes" ] && [ ! -d "${JAVA_HOME}" ]; then
@@ -110,9 +110,9 @@ if [ "${has_java_home}" = "yes" ]; then
       export JAVA21_HOME="${JAVA_HOME}"
       has_java21="yes"
     fi
-    if [ "${has_java22}" = "no" ] && [ "${java_version}" = 22 ]; then
-      export JAVA22_HOME="${JAVA_HOME}"
-      has_java22="yes"
+    if [ "${has_java23}" = "no" ] && [ "${java_version}" = 23 ]; then
+      export JAVA23_HOME="${JAVA_HOME}"
+      has_java23="yes"
     fi
 fi
 
@@ -136,23 +136,23 @@ if [ "${has_java21}" = "yes" ] && [ ! -d "${JAVA21_HOME}" ]; then
     exit 1
 fi
 
-if [ "${has_java22}" = "yes" ] && [ ! -d "${JAVA22_HOME}" ]; then
-    echo "JAVA22_HOME is set to a non-existent directory ${JAVA22_HOME}"
+if [ "${has_java23}" = "yes" ] && [ ! -d "${JAVA23_HOME}" ]; then
+    echo "JAVA23_HOME is set to a non-existent directory ${JAVA23_HOME}"
     exit 1
 fi
 
-if [ "${has_java8}" = "no" ] && [ "${has_java11}" = "no" ] && [ "${has_java17}" = "no" ] && [ "${has_java21}" = "no" ] && [ "${has_java22}" = "no" ]; then
+if [ "${has_java8}" = "no" ] && [ "${has_java11}" = "no" ] && [ "${has_java17}" = "no" ] && [ "${has_java21}" = "no" ] && [ "${has_java23}" = "no" ]; then
     if [ "${has_java_home}" = "yes" ]; then
       echo "Cannot determine Java version from JAVA_HOME"
     else
-      echo "No Java 8, 11, 17, 21, or 22 JDKs found. At least one of JAVA_HOME, JAVA8_HOME, JAVA11_HOME, JAVA17_HOME, JAVA21_HOME, or JAVA22_HOME must be set."
+      echo "No Java 8, 11, 17, 21, or 23 JDKs found. At least one of JAVA_HOME, JAVA8_HOME, JAVA11_HOME, JAVA17_HOME, JAVA21_HOME, or JAVA23_HOME must be set."
     fi
     echo "JAVA_HOME = ${JAVA_HOME}"
     echo "JAVA8_HOME = ${JAVA8_HOME}"
     echo "JAVA11_HOME = ${JAVA11_HOME}"
     echo "JAVA17_HOME = ${JAVA17_HOME}"
     echo "JAVA21_HOME = ${JAVA21_HOME}"
-    echo "JAVA22_HOME = ${JAVA22_HOME}"
+    echo "JAVA23_HOME = ${JAVA23_HOME}"
     command -v java
     java -version
     exit 1
diff --git a/checker/bin/wpi.sh b/checker/bin/wpi.sh
index b8bb85ead09..90c896e070b 100755
--- a/checker/bin/wpi.sh
+++ b/checker/bin/wpi.sh
@@ -75,11 +75,11 @@ else
   has_java21="yes"
 fi
 
-# shellcheck disable=SC2153 # testing for JAVA22_HOME, not a typo of JAVA_HOME
-if [ "${JAVA22_HOME}" = "" ]; then
-  has_java22="no"
+# shellcheck disable=SC2153 # testing for JAVA23_HOME, not a typo of JAVA_HOME
+if [ "${JAVA23_HOME}" = "" ]; then
+  has_java23="no"
 else
-  has_java22="yes"
+  has_java23="yes"
 fi
 
 if [ "${has_java_home}" = "yes" ] && [ ! -d "${JAVA_HOME}" ]; then
@@ -105,9 +105,9 @@ if [ "${has_java_home}" = "yes" ]; then
       export JAVA21_HOME="${JAVA_HOME}"
       has_java21="yes"
     fi
-    if [ "${has_java22}" = "no" ] && [ "${java_version}" = 22 ]; then
-      export JAVA22_HOME="${JAVA_HOME}"
-      has_java22="yes"
+    if [ "${has_java23}" = "no" ] && [ "${java_version}" = 23 ]; then
+      export JAVA23_HOME="${JAVA_HOME}"
+      has_java23="yes"
     fi
 fi
 
@@ -131,23 +131,23 @@ if [ "${has_java21}" = "yes" ] && [ ! -d "${JAVA21_HOME}" ]; then
     exit 9
 fi
 
-if [ "${has_java22}" = "yes" ] && [ ! -d "${JAVA22_HOME}" ]; then
-    echo "JAVA22_HOME is set to a non-existent directory ${JAVA22_HOME}"
+if [ "${has_java23}" = "yes" ] && [ ! -d "${JAVA23_HOME}" ]; then
+    echo "JAVA23_HOME is set to a non-existent directory ${JAVA23_HOME}"
     exit 10
 fi
 
-if [ "${has_java8}" = "no" ] && [ "${has_java11}" = "no" ] && [ "${has_java17}" = "no" ] && [ "${has_java21}" = "no" ] && [ "${has_java22}" = "no" ]; then
+if [ "${has_java8}" = "no" ] && [ "${has_java11}" = "no" ] && [ "${has_java17}" = "no" ] && [ "${has_java21}" = "no" ] && [ "${has_java23}" = "no" ]; then
     if [ "${has_java_home}" = "yes" ]; then
       echo "Cannot determine Java version from JAVA_HOME"
     else
-      echo "No Java 8, 11, 17, 21, or 22 JDKs found. At least one of JAVA_HOME, JAVA8_HOME, JAVA11_HOME, JAVA17_HOME, JAVA21_HOME, or JAVA22_HOME must be set."
+      echo "No Java 8, 11, 17, 21, or 23 JDKs found. At least one of JAVA_HOME, JAVA8_HOME, JAVA11_HOME, JAVA17_HOME, JAVA21_HOME, or JAVA23_HOME must be set."
     fi
     echo "JAVA_HOME = ${JAVA_HOME}"
     echo "JAVA8_HOME = ${JAVA8_HOME}"
     echo "JAVA11_HOME = ${JAVA11_HOME}"
     echo "JAVA17_HOME = ${JAVA17_HOME}"
     echo "JAVA21_HOME = ${JAVA21_HOME}"
-    echo "JAVA22_HOME = ${JAVA22_HOME}"
+    echo "JAVA23_HOME = ${JAVA23_HOME}"
     command -v java
     java -version
     exit 11
diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalVisitor.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalVisitor.java
index c2d8aca90fc..70a74f9d4dd 100644
--- a/checker/src/main/java/org/checkerframework/checker/optional/OptionalVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalVisitor.java
@@ -505,7 +505,7 @@ public Void visitVariable(VariableTree tree, Void p) {
    * {@code x = Optional.of(Optional.of("baz"));}. However, the type of the right-hand side is
    * {@code Optional<? extends Object>}, not {@code Optional<Optional<String>>}. Therefore, to fully
    * check for improper types, it is necessary to examine, in the type checker, the argument to
-   * construction of an Optional. Method {@link handleNestedOptionalCreation} does so.
+   * construction of an Optional. Method {@link #handleNestedOptionalCreation} does so.
    */
   private final class OptionalTypeValidator extends BaseTypeValidator {
 
diff --git a/checker/tests/i18n-formatter/Syntax.java b/checker/tests/i18n-formatter/Syntax.java
index 8665aef0e43..71bc00c1d98 100644
--- a/checker/tests/i18n-formatter/Syntax.java
+++ b/checker/tests/i18n-formatter/Syntax.java
@@ -83,8 +83,9 @@ public static void invalidSubformatPattern() {
     MessageFormat.format("{0, number, #.#.#}", 1);
     // :: error: (i18nformat.string)
     MessageFormat.format("{0, date, y.m.d.x}", new Date());
-    // :: error: (i18nformat.string)
-    MessageFormat.format("{0, choice, 0##zero}", 0);
+    // This seems to be permitted by Java 23.
+    // // :: error: (i18nformat.string)
+    // MessageFormat.format("{0, choice, 0##zero}", 0);
 
     // good
     MessageFormat.format("{0, number, #.#}", 1);
diff --git a/checker/tests/wpi-many/testin.txt b/checker/tests/wpi-many/testin.txt
index d0b80a19068..cb28c0c3d07 100644
--- a/checker/tests/wpi-many/testin.txt
+++ b/checker/tests/wpi-many/testin.txt
@@ -1,7 +1,7 @@
-https://github.com/kelloggm/wpi-many-tests-bcel-util a67f0cd3f59f621cffd0567306df55766f17550a
-https://github.com/kelloggm/wpi-many-tests-bibtex-clean 43e0372475bf8d08522197b5b50196e8176b658b
-https://github.com/kelloggm/wpi-many-tests-ensures-called-methods 5f39f1e5ad364900b5542438bae0a562db230d20
-https://github.com/kelloggm/wpi-many-tests-html-pretty-print c3ce7959c68c1ecc40d8c85c31080bcc59f2854e
-https://github.com/kelloggm/-wpi-many-tests-bibtex-clean 8e0d2c17240056ccd7d45efa272fb364aa482617
+https://github.com/kelloggm/wpi-many-tests-bcel-util 91415634c1d47ada93de4fb9105bbd7817928a58
+https://github.com/kelloggm/wpi-many-tests-bibtex-clean fe7ae9a276d8d392c174d497c14a7bf4f30876e8
+https://github.com/kelloggm/wpi-many-tests-ensures-called-methods e5ad4c582392ee8edd8a6270b12aad876df94782
+https://github.com/kelloggm/wpi-many-tests-html-pretty-print de5790094a1b3cece9cd97152a5c54afa615e6d9
+https://github.com/kelloggm/-wpi-many-tests-bibtex-clean 4da53d845f91e5a34987f70227ec6e5b11e8fc60
 # This comment line tests that the commenting feature works (if it doesn't, then this line will be read and fail, as it's not a URL).
 https://github.com/Nargeshdb/wpi-many-tests-owning-field f446e987fdb87a4c8364c9a2728be70900cb30d5
diff --git a/dataflow/build.gradle b/dataflow/build.gradle
index 060edd876cd..71921f2515f 100644
--- a/dataflow/build.gradle
+++ b/dataflow/build.gradle
@@ -10,6 +10,8 @@ dependencies {
   // Node implements org.plumelib.util.UniqueId, so this dependency must be "api".
   api "org.plumelib:plume-util:${versions.plumeUtil}"
 
+  implementation "org.plumelib:hashmap-util:${versions.hashmapUtil}"
+
   // External dependencies:
   // If you add an external dependency, you must shadow its packages both in the dataflow-shaded
   // artifact (see shadowJar block below) and also in checker.jar (see the comment in
diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md
index 8d59552372d..52c0c6141f1 100644
--- a/docs/CHANGELOG.md
+++ b/docs/CHANGELOG.md
@@ -4,6 +4,7 @@ Version 3.46.1 (September 3, 2024)
 **User-visible changes:**
 
 The Checker Framework runs under JDK 22 -- that is, it runs on a version 22 JVM.
+The Checker Framework runs under JDK 23 -- that is, it runs on a version 23 JVM.
 
 **Implementation details:**
 
diff --git a/docs/developer/developer-manual.html b/docs/developer/developer-manual.html
index a9bd894c558..38557d904e4 100644
--- a/docs/developer/developer-manual.html
+++ b/docs/developer/developer-manual.html
@@ -48,6 +48,7 @@ <h1 id="Checker_Framework_developer_manual">Checker Framework developer manual</
       <li><a href="#Documenting_refactoring_ideas">Documenting refactoring ideas</a></li>
       <li><a href="#annotated-library-version-numbers">Version numbers for annotated libraries</a></li>
       <li><a href="#Making_a_Checker_Framework_release">Making a Checker Framework release</a></li>
+      <li><a href="#Supporting_a_new_version_of_Java">Supporting a new version of Java</a></li>
       <li><a href="#Case_studies">Describing a case study</a></li>
       <li><a href="#Counting_annotations">Counting annotations</a></li>
       <li><a href="#Build_historical">Building a historical version of the Checker Framework</a></li>
@@ -530,6 +531,43 @@ <h2 id="Making_a_Checker_Framework_release">Making a Checker Framework release</
 </p>
 
 
+<h2 id="Supporting_a_new_version_of_Java">Supporting a new version of Java</h2>
+
+<p>
+To upgrade the Checker Framework to use a newer version of Java:
+</p>
+
+<pre>
+# Create a branch named "java-23".
+cd $t/checker-framework-fork-mernst-branch-master
+gnb java-23
+cd $t/checker-framework-fork-mernst-branch-java-23
+
+# Edit:
+checker/bin/wpi.sh
+checker/bin/wpi-many.sh (diff it against wpi.sh)
+# Rename and edit:
+checker/bin-devel/Dockerfile-ubuntu-jdkXX
+checker/bin-devel/Dockerfile-ubuntu-jdkXX-plus (diff it against Dockerfile-ubuntu-jdkXX)
+# Further search for: (java|jdk).?22\b
+# Don't push changes yet.
+
+# Use the latest version of Gradle, which supports the new JDK version
+# (see https://docs.gradle.org/current/userguide/compatibility.html):
+for wmtest in wpi-many-tests-bcel-util wpi-many-tests-bibtex-clean wpi-many-tests-ensures-called-methods wpi-many-tests-html-pretty-print wpi-many-tests-owning-field -wpi-many-tests-bibtex-clean ; do
+  cd $t/$wmtest && \
+  (./gradlew wrapper --gradle-version 8.10 && ./gradlew build --warning-mode=all) && \
+  git commit -m "Use Gradle 8.10" gradle/wrapper/gradle-wrapper.properties && \
+  git push
+done
+# Now update file checker/tests/wpi-many/testin.txt.
+
+# Build the Docker images for the newest JDK version (others need not be rebuilt).
+
+# Push changes.  Fix any build failures.
+</pre>
+
+
 <h2 id="Case_studies">Describing a case study</h2>
 
 <p>
diff --git a/docs/examples/lombok/Makefile b/docs/examples/lombok/Makefile
index cd334d719ef..b2c0a7684a2 100644
--- a/docs/examples/lombok/Makefile
+++ b/docs/examples/lombok/Makefile
@@ -4,8 +4,8 @@ JAVA_VER := $(shell java -version 2>&1 | head -1 | cut -d'"' -f2 | sed '/^1\./s/
 
 # Delomboking seems to mess up line numbers. The actual error is on line 13, but the error appears on line 12.
 # So check for both the error message and make sure it is for the right assignment.
-# As of 2020-09-23, lombok does not work under Java 22, see https://projectlombok.org/changelog .
-ifeq (${JAVA_VER},22)
+# As of 2020-09-23, lombok does not work under Java 23, see https://projectlombok.org/changelog .
+ifeq (${JAVA_VER},23)
 all:
 	@echo "Skipping test because lombok does not work under Java ${JAVA_VER}"
 else
diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
index 3e605e09604..5186a251c49 100644
--- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
+++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java
@@ -283,6 +283,7 @@ public class AnnotatedTypeFactory implements AnnotationProvider {
   protected QualifierHierarchy qualHierarchy;
 
   /** Represent the type relations. */
+  // This field cannot be final because it is set in `postInit()`.
   protected TypeHierarchy typeHierarchy;
 
   /** Performs whole-program inference. If null, whole-program inference is disabled. */
diff --git a/javacutil/build.gradle b/javacutil/build.gradle
index 806b1963d55..fe2a25b6d81 100644
--- a/javacutil/build.gradle
+++ b/javacutil/build.gradle
@@ -15,6 +15,7 @@ dependencies {
 
   // This is used by org.checkerframework.javacutil.TypesUtils.isImmutableTypeInJdk.
   // https://mvnrepository.com/artifact/org.plumelib/plume-util
+  implementation "org.plumelib:hashmap-util:${versions.hashmapUtil}"
   implementation "org.plumelib:plume-util:${versions.plumeUtil}"
   implementation "org.plumelib:reflection-util:${versions.reflectionUtil}"
 
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/Resolver.java b/javacutil/src/main/java/org/checkerframework/javacutil/Resolver.java
index 77e7104ec16..3ca9369e714 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/Resolver.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/Resolver.java
@@ -65,6 +65,9 @@ public class Resolver {
   /** Whether we are running on at least Java 13. */
   private static final boolean atLeastJava13 = sourceVersionNumber >= 13;
 
+  /** Whether we are running on at least Java 23. */
+  private static final boolean atLeastJava23 = sourceVersionNumber >= 23;
+
   static {
     try {
       FIND_METHOD =
@@ -79,7 +82,13 @@ public class Resolver {
               boolean.class);
       FIND_METHOD.setAccessible(true);
 
-      FIND_VAR = Resolve.class.getDeclaredMethod("findVar", Env.class, Name.class);
+      if (atLeastJava23) {
+        FIND_VAR =
+            Resolve.class.getDeclaredMethod(
+                "findVar", DiagnosticPosition.class, Env.class, Name.class);
+      } else {
+        FIND_VAR = Resolve.class.getDeclaredMethod("findVar", Env.class, Name.class);
+      }
       FIND_VAR.setAccessible(true);
 
       if (atLeastJava13) {
@@ -128,7 +137,7 @@ public class Resolver {
       FIND_TYPE.setAccessible(true);
     } catch (Exception e) {
       Error err =
-          new AssertionError("Compiler 'Resolve' class doesn't contain required 'find' method");
+          new AssertionError("Compiler 'Resolve' class doesn't contain required 'find*' method");
       err.initCause(e);
       throw err;
     }
@@ -275,7 +284,12 @@ public Env<AttrContext> getEnvForPath(TreePath path) {
     try {
       Env<AttrContext> env = getEnvForPath(path);
       // Either a VariableElement or a SymbolNotFoundError.
-      Element res = wrapInvocationOnResolveInstance(FIND_VAR, env, names.fromString(name));
+      Element res;
+      if (atLeastJava23) {
+        res = wrapInvocationOnResolveInstance(FIND_VAR, null, env, names.fromString(name));
+      } else {
+        res = wrapInvocationOnResolveInstance(FIND_VAR, env, names.fromString(name));
+      }
       // Every kind in the documentation of Element.getKind() is explicitly tested, possibly
       // in the "default:" case.
       switch (res.getKind()) {