diff --git a/proofs/cbmc/Makefile.common b/proofs/cbmc/Makefile.common
index 84f0cc33c0..7cf25d8806 100644
--- a/proofs/cbmc/Makefile.common
+++ b/proofs/cbmc/Makefile.common
@@ -191,7 +191,7 @@ CBMC_DM_ILP32_CBMC_FLAG := --ILP32
 CBMC_DM_ILP32_INCLUDE := $(CBMC_ROOT)/cbmc/include/ILP32
 
 # Solver profile IDs name the executable and all solver-specific options.
-CBMC_SOLVER_PROFILES_ALL := z3 z3_smt_only z3_no_bv_extract bitwuzla cvc5_arrays_exp cvc5_mbqi_enum cvc5_enum_inst
+CBMC_SOLVER_PROFILES_ALL := z3 z3_smt_only z3_no_bv_extract bitwuzla cvc5_arrays_exp cvc5_mbqi_enum cvc5_enum_inst cadical
 
 CBMC_PROFILE_z3_BACKEND := --smt2
 CBMC_PROFILE_z3_PROVER_NAME := Z3
@@ -230,6 +230,11 @@ CBMC_PROFILE_cvc5_enum_inst_PROVER_NAME := cvc5
 CBMC_PROFILE_cvc5_enum_inst_SMT_FORMAT := --cvc5
 CBMC_PROFILE_cvc5_enum_inst_FLAGS := --external-smt2-solver $(PROOF_ROOT)/lib/cvc5_enum_inst --cvc5
 
+CBMC_PROFILE_cadical_BACKEND :=
+CBMC_PROFILE_cadical_PROVER_NAME := CaDiCaL
+CBMC_PROFILE_cadical_SMT_FORMAT :=
+CBMC_PROFILE_cadical_FLAGS := --sat-solver cadical
+
 # Make evaluates the configuration checks below before running target recipes.
 # The runner queries these metadata targets before selecting CBMC_DM/CBMC_SOLVER.
 CBMC_INTROSPECTION_TARGETS := echo-supported-configs echo-default-config echo-solver-profiles echo-data-models echo-proof-uid echo-project-name litani-path
diff --git a/proofs/cbmc/compute_pack_z/Makefile b/proofs/cbmc/compute_pack_z/Makefile
index bf46be9fba..e1146f47fe 100644
--- a/proofs/cbmc/compute_pack_z/Makefile
+++ b/proofs/cbmc/compute_pack_z/Makefile
@@ -34,7 +34,9 @@ APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Supported CBMC configurations
-CBMC_SUPPORTED_CONFIGS = LP64:z3_no_bv_extract
+CBMC_SUPPORTED_CONFIGS = \
+  LP64:z3_no_bv_extract \
+  LP64:cadical
 CBMC_DEFAULT_CONFIG = LP64:z3_no_bv_extract
 
 FUNCTION_NAME = mld_compute_pack_z
diff --git a/proofs/cbmc/pointwise_acc_native_x86_64/Makefile b/proofs/cbmc/pointwise_acc_native_x86_64/Makefile
index 00e9d2a0fe..ab36c204be 100644
--- a/proofs/cbmc/pointwise_acc_native_x86_64/Makefile
+++ b/proofs/cbmc/pointwise_acc_native_x86_64/Makefile
@@ -36,7 +36,9 @@ APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Supported CBMC configurations
-CBMC_SUPPORTED_CONFIGS = LP64:z3_smt_only
+CBMC_SUPPORTED_CONFIGS = \
+  LP64:z3_smt_only \
+  LP64:cadical
 CBMC_DEFAULT_CONFIG = LP64:z3_smt_only
 
 FUNCTION_NAME = pointwise_acc_native_x86_64
diff --git a/proofs/cbmc/poly_decompose_32_native_aarch64/Makefile b/proofs/cbmc/poly_decompose_32_native_aarch64/Makefile
index 27139cc81e..71b4c10876 100644
--- a/proofs/cbmc/poly_decompose_32_native_aarch64/Makefile
+++ b/proofs/cbmc/poly_decompose_32_native_aarch64/Makefile
@@ -36,7 +36,9 @@ APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Supported CBMC configurations
-CBMC_SUPPORTED_CONFIGS = LP64:z3
+CBMC_SUPPORTED_CONFIGS = \
+  LP64:z3 \
+  LP64:cadical
 CBMC_DEFAULT_CONFIG = LP64:z3
 
 FUNCTION_NAME = poly_decompose_32_native_aarch64
diff --git a/proofs/cbmc/poly_decompose_native/Makefile b/proofs/cbmc/poly_decompose_native/Makefile
index 4179382cf2..a3bdf52e1d 100644
--- a/proofs/cbmc/poly_decompose_native/Makefile
+++ b/proofs/cbmc/poly_decompose_native/Makefile
@@ -32,7 +32,9 @@ APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Supported CBMC configurations
-CBMC_SUPPORTED_CONFIGS = LP64:z3
+CBMC_SUPPORTED_CONFIGS = \
+  LP64:z3 \
+  LP64:cadical
 CBMC_DEFAULT_CONFIG = LP64:z3
 
 FUNCTION_NAME = poly_decompose_native
diff --git a/proofs/cbmc/poly_decompose_native_x86_64/Makefile b/proofs/cbmc/poly_decompose_native_x86_64/Makefile
index 5a9a3508c3..ca16d24e7f 100644
--- a/proofs/cbmc/poly_decompose_native_x86_64/Makefile
+++ b/proofs/cbmc/poly_decompose_native_x86_64/Makefile
@@ -36,7 +36,9 @@ APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Supported CBMC configurations
-CBMC_SUPPORTED_CONFIGS = LP64:z3
+CBMC_SUPPORTED_CONFIGS = \
+  LP64:z3 \
+  LP64:cadical
 CBMC_DEFAULT_CONFIG = LP64:z3
 
 FUNCTION_NAME = poly_decompose_native_x86_64
diff --git a/proofs/cbmc/poly_uniform_gamma1/Makefile b/proofs/cbmc/poly_uniform_gamma1/Makefile
index 6ce7c4feb1..8064567739 100644
--- a/proofs/cbmc/poly_uniform_gamma1/Makefile
+++ b/proofs/cbmc/poly_uniform_gamma1/Makefile
@@ -36,7 +36,9 @@ APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Supported CBMC configurations
-CBMC_SUPPORTED_CONFIGS = LP64:z3
+CBMC_SUPPORTED_CONFIGS = \
+  LP64:z3 \
+  LP64:cadical
 CBMC_DEFAULT_CONFIG = LP64:z3
 
 FUNCTION_NAME = poly_uniform_gamma1
diff --git a/proofs/cbmc/poly_uniform_gamma1_4x/Makefile b/proofs/cbmc/poly_uniform_gamma1_4x/Makefile
index 949d28b95a..9f837c237c 100644
--- a/proofs/cbmc/poly_uniform_gamma1_4x/Makefile
+++ b/proofs/cbmc/poly_uniform_gamma1_4x/Makefile
@@ -33,7 +33,9 @@ APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Supported CBMC configurations
-CBMC_SUPPORTED_CONFIGS = LP64:z3
+CBMC_SUPPORTED_CONFIGS = \
+  LP64:z3 \
+  LP64:cadical
 CBMC_DEFAULT_CONFIG = LP64:z3
 
 FUNCTION_NAME = poly_uniform_gamma1_4x
diff --git a/proofs/cbmc/sample_pack_s1_s2/Makefile b/proofs/cbmc/sample_pack_s1_s2/Makefile
index 8f1f2764d5..0058a3a5f0 100644
--- a/proofs/cbmc/sample_pack_s1_s2/Makefile
+++ b/proofs/cbmc/sample_pack_s1_s2/Makefile
@@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Supported CBMC configurations
-CBMC_SUPPORTED_CONFIGS = LP64:z3
+CBMC_SUPPORTED_CONFIGS = \
+  LP64:z3 \
+  LP64:cadical
 CBMC_DEFAULT_CONFIG = LP64:z3
 
 FUNCTION_NAME = mld_sample_pack_s1_s2
diff --git a/proofs/cbmc/sign_signature_extmu/Makefile b/proofs/cbmc/sign_signature_extmu/Makefile
index 2a17cac772..52f2adde5b 100644
--- a/proofs/cbmc/sign_signature_extmu/Makefile
+++ b/proofs/cbmc/sign_signature_extmu/Makefile
@@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Supported CBMC configurations
-CBMC_SUPPORTED_CONFIGS = LP64:z3
+CBMC_SUPPORTED_CONFIGS = \
+  LP64:z3 \
+  LP64:cadical
 CBMC_DEFAULT_CONFIG = LP64:z3
 
 FUNCTION_NAME = sign_signature_extmu
diff --git a/proofs/cbmc/unpack_sk/Makefile b/proofs/cbmc/unpack_sk/Makefile
index 9753f2e370..b80877e450 100644
--- a/proofs/cbmc/unpack_sk/Makefile
+++ b/proofs/cbmc/unpack_sk/Makefile
@@ -27,7 +27,9 @@ APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
 # Supported CBMC configurations
-CBMC_SUPPORTED_CONFIGS = LP64:z3
+CBMC_SUPPORTED_CONFIGS = \
+  LP64:z3 \
+  LP64:cadical
 CBMC_DEFAULT_CONFIG = LP64:z3
 
 FUNCTION_NAME = unpack_sk