diff --git a/.gitignore b/.gitignore
index 82d2291fd22b0..a98335bf7c3e4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -49,8 +49,8 @@ package-lock.json
 ## Kani
 *.out
 
-## GOTO-Transcoder
-goto-transcoder
+## ESBMC
+esbmc
 # Added by cargo
 #
 # already existing elements were commented out
diff --git a/scripts/run-goto-transcoder.sh b/scripts/run-goto-transcoder.sh
index e11a012ed4556..f605e5714152e 100755
--- a/scripts/run-goto-transcoder.sh
+++ b/scripts/run-goto-transcoder.sh
@@ -5,48 +5,57 @@ set -e
 ##############
 # PARAMETERS #
 ##############
-contract_folder=$1/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps
+target=$1/kani_verify_std/target/x86_64-unknown-linux-gnu/debug
 supported_regex=$2
 unsupported_regex=neg
 
-goto_transcoder_git=https://github.com/esbmc/goto-transcoder
-esbmc_url=https://github.com/esbmc/esbmc/releases/download/v7.10/esbmc-linux.zip
+# ESBMC reads CBMC goto binaries directly since v8.4, so Kani's output needs no conversion.
+esbmc_url=https://github.com/esbmc/esbmc/releases/download/v8.5/esbmc-linux.zip
+esbmc=esbmc/release/bin/esbmc
+
+contract_folder=$target/deps
+# Cargo 1.99+ gives each package its own debug/build/PKG/HASH/out/ and no longer creates debug/deps.
+if [ ! -d "$contract_folder" ]; then
+    contract_folder=$(find "$target/build" -path '*/out/*.out' | grep "$supported_regex" | head -n 1 | xargs -r dirname)
+fi
+if [ -z "$contract_folder" ]; then
+    echo "No contract programs matching '$supported_regex' under $target"
+    exit 1
+fi
 
 ##########
 # SCRIPT #
 ##########
 
-echo "Checking contracts with goto-transcoder"
+echo "Checking contracts with ESBMC"
 
-if [ ! -d "goto-transcoder" ]; then
-    echo "goto-transcoder not found. Downloading..."
-    git clone $goto_transcoder_git
-    cd goto-transcoder
-    wget $esbmc_url
-    unzip esbmc-linux.zip
-    chmod +x ./bin/esbmc
-    cd ..
+if [ ! -x "$esbmc" ]; then
+    echo "ESBMC not found. Downloading..."
+    mkdir -p esbmc
+    wget -q -O esbmc/esbmc-linux.zip $esbmc_url
+    unzip -q -o esbmc/esbmc-linux.zip -d esbmc
+    chmod +x $esbmc
 fi
 
-ls $contract_folder | grep "$supported_regex" | grep -v .symtab.out > ./goto-transcoder/_contracts.txt
+checked=0
+ls $contract_folder | grep "$supported_regex" | grep -v .symtab.out > _contracts.txt
 
-cd goto-transcoder
 while IFS= read -r line; do
     # I expect each line to be similar to 'core-58cefd8dce4133f9__RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8.out'
     # The entrypoint of the contract would be _RNvNtNtCs9uKEoH8KKW4_4core3num6verify24checked_unchecked_add_i8
-    # So we use awk to extract this name.
-    contract=`echo "$line" | awk '{match($0, /(_RNv.*).out/, arr); print arr[1]}'`
-    echo "Processing: $contract"
-    if [[ -z "$contract" ]]; then
-        continue
-    fi
+    [[ $line =~ (_RNv.*)\.out$ ]] || continue
+    contract=${BASH_REMATCH[1]}
     if echo "$contract" | grep -q "$unsupported_regex"; then
         continue
     fi
-    echo "Running: goto-transcoder $contract $contract_folder/$line $contract.esbmc.goto"
-    cargo run cbmc2esbmc  ../$contract_folder/$line $contract.esbmc.goto
-    ./bin/esbmc --cprover --function $contract --binary resources/library.goto $contract.esbmc.goto
+    echo "Processing: $contract"
+    $esbmc --binary $contract_folder/$line --function $contract < /dev/null
+    checked=$((checked + 1))
 done < "_contracts.txt"
 
 rm "_contracts.txt"
-cd ..
+
+if [ "$checked" -eq 0 ]; then
+    echo "No contract matching '$supported_regex' was checked"
+    exit 1
+fi