diff --git a/CHANGELOG.md b/CHANGELOG.md
index bf10e7cbc..6067566c6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,7 @@ This release is available in the following languages:
 ### Features
 
 - **SharedCache:** Shared Cache for Searchable Encryption ([#1476](https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1476)) ([46076f8](https://github.com/aws/aws-database-encryption-sdk-dynamodb/commit/46076f86aec77f7df204c1e06a8ecb2400f01b6f))
+- bump to dafny 4.9.0 and mpl 1.9.0 ([#1627](https://github.com/aws/aws-database-encryption-sdk-dynamodb/pull/1627))
 
 ### Fixes
 
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
index 6e974d03c..d8a0c3dc9 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
@@ -176,7 +176,7 @@ module SearchConfigToInfo {
     var cache;
     if cacheType.Shared? {
       cache := cacheType.Shared;
-      reveal ValidSharedCache(config);
+      reveal ValidSharedCache();
     } else {
       //= specification/searchable-encryption/search-config.md#key-store-cache
       //# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md)
diff --git a/codebuild/release/release-prod.yml b/codebuild/release/release-prod.yml
index 0f578bbf5..7a167c659 100644
--- a/codebuild/release/release-prod.yml
+++ b/codebuild/release/release-prod.yml
@@ -19,7 +19,7 @@ phases:
     commands:
       - cd ..
       # Get Dafny
-      - curl https://github.com/dafny-lang/dafny/releases/download/v4.8.0/dafny-4.8.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
+      - curl https://github.com/dafny-lang/dafny/releases/download/v4.9.0/dafny-4.9.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
       - unzip -qq dafny.zip && rm dafny.zip
       - export PATH="$PWD/dafny:$PATH"
       # Get Gradle 7.6
diff --git a/codebuild/release/validate-release.yml b/codebuild/release/validate-release.yml
index 3235615ac..5c0007a1a 100644
--- a/codebuild/release/validate-release.yml
+++ b/codebuild/release/validate-release.yml
@@ -14,7 +14,7 @@ phases:
     commands:
       - cd ..
       # Get Dafny
-      - curl https://github.com/dafny-lang/dafny/releases/download/v4.8.0/dafny-4.8.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
+      - curl https://github.com/dafny-lang/dafny/releases/download/v4.9.0/dafny-4.9.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
       - unzip -qq dafny.zip && rm dafny.zip
       - export PATH="$PWD/dafny:$PATH"
       # Get Gradle 7.6
diff --git a/codebuild/staging/release-staging.yml b/codebuild/staging/release-staging.yml
index 541dbe66d..1fd288949 100644
--- a/codebuild/staging/release-staging.yml
+++ b/codebuild/staging/release-staging.yml
@@ -21,7 +21,7 @@ phases:
     commands:
       - cd ..
       # Get Dafny
-      - curl https://github.com/dafny-lang/dafny/releases/download/v4.8.0/dafny-4.8.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
+      - curl https://github.com/dafny-lang/dafny/releases/download/v4.9.0/dafny-4.9.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
       - unzip -qq dafny.zip && rm dafny.zip
       - export PATH="$PWD/dafny:$PATH"
       # Get Gradle 7.6
diff --git a/codebuild/staging/validate-staging.yml b/codebuild/staging/validate-staging.yml
index 0b57ac93c..6bd1cd9cf 100644
--- a/codebuild/staging/validate-staging.yml
+++ b/codebuild/staging/validate-staging.yml
@@ -18,7 +18,7 @@ phases:
     commands:
       - cd ..
       # Get Dafny
-      - curl https://github.com/dafny-lang/dafny/releases/download/v4.8.0/dafny-4.8.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
+      - curl https://github.com/dafny-lang/dafny/releases/download/v4.9.0/dafny-4.9.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
       - unzip -qq dafny.zip && rm dafny.zip
       - export PATH="$PWD/dafny:$PATH"
       # Get Gradle 7.6