diff --git a/cbmc.h b/cbmc.h
index 452390f..daac15d 100644
--- a/cbmc.h
+++ b/cbmc.h
@@ -32,6 +32,11 @@
 /* cassert to avoid confusion with in-built assert */
 #define cassert(x) __CPROVER_assert(x, "cbmc assertion failed")
 #define assume(...) __CPROVER_assume(__VA_ARGS__)
+/* https://diffblue.github.io/cbmc/contracts-function-pointer-predicates.html */
+#define obeys_contract(...) __CPROVER_obeys_contract(__VA_ARGS__)
+
+
+
 
 /***************************************************
  * Macros for "expression" forms that may appear
diff --git a/proofs/cbmc/wots_sign/Makefile b/proofs/cbmc/wots_sign/Makefile
new file mode 100644
index 0000000..defd493
--- /dev/null
+++ b/proofs/cbmc/wots_sign/Makefile
@@ -0,0 +1,54 @@
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = wots_sign_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = wots_sign
+
+DEFINES +=
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/slh_dsa.c
+
+CHECK_FUNCTION_CONTRACTS=wots_sign
+USE_FUNCTION_CONTRACTS=get_len wots_csum adrs_set_chain_address
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+RESTRICT_FUNCTION_POINTER=wots_sign.function_pointer_call.1/wots_chain_contract
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--smt2
+
+FUNCTION_NAME = wots_sign
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 8
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mlkem/src/poly.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/src/poly.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common
diff --git a/proofs/cbmc/wots_sign/wots_sign_harness.c b/proofs/cbmc/wots_sign/wots_sign_harness.c
new file mode 100644
index 0000000..d18fa32
--- /dev/null
+++ b/proofs/cbmc/wots_sign/wots_sign_harness.c
@@ -0,0 +1,17 @@
+// Copyright (c) The slhdsa-c project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include <stddef.h>
+#include <stdint.h>
+#include <string.h>
+#include "slh_var.h"
+
+size_t wots_sign(slh_var_t *var, uint8_t *sig, const uint8_t *m);
+
+void harness(void)
+{
+  slh_var_t *var;
+  uint8_t *sig;
+  uint8_t *m;
+  wots_sign(var, sig, m);
+}
diff --git a/slh_adrs.h b/slh_adrs.h
index 8bd0ac8..d6113ce 100644
--- a/slh_adrs.h
+++ b/slh_adrs.h
@@ -108,6 +108,8 @@ static SLH_INLINE void adrs_set_tree_height(slh_var_t *var, uint32_t x)
 
 /* === Set WOTS+ chain address. */
 static SLH_INLINE void adrs_set_chain_address(slh_var_t *var, uint32_t x)
+/* TODO: complete*/
+__contract__()
 {
   var->adrs->u32[6] = rev8_be32(x);
 }
diff --git a/slh_dsa.c b/slh_dsa.c
index 4fb3dad..ee1a930 100644
--- a/slh_dsa.c
+++ b/slh_dsa.c
@@ -44,6 +44,10 @@ static SLH_INLINE uint32_t gen_len2(const slh_param_t *prm)
 }
 
 static SLH_INLINE uint32_t get_len(const slh_param_t *prm)
+/* TODO: complete*/
+__contract__(
+  ensures(return_value < SLH_MAX_LEN)
+)
 {
   return get_len1(prm) + gen_len2(prm);
 }
@@ -93,6 +97,8 @@ static SLH_INLINE size_t base_2b(uint32_t *v, const uint8_t *x, uint32_t b,
 
 /* (wots_csum is a shared helper function for algorithms 7 and 8) */
 static void wots_csum(uint32_t *vm, const uint8_t *m, const slh_param_t *prm)
+/* TODO: complete*/
+__contract__()
 {
   uint32_t csum, i, t;
   uint32_t len1, len2;
@@ -119,6 +125,14 @@ static void wots_csum(uint32_t *vm, const uint8_t *m, const slh_param_t *prm)
 }
 
 static size_t wots_sign(slh_var_t *var, uint8_t *sig, const uint8_t *m)
+__contract__(
+  requires(memory_no_alias(var, sizeof(slh_var_t)))
+  requires(memory_no_alias(var->prm, sizeof(slh_param_t)))
+  requires(var->prm->n <= SLH_MAX_N)
+  requires(obeys_contract(var->prm->wots_chain, wots_chain_contract))
+  requires(memory_no_alias(sig, var->prm->n * SLH_MAX_LEN))
+  assigns(object_whole(sig))
+)
 {
   const slh_param_t *prm = var->prm;
   uint32_t i, len;
@@ -129,6 +143,11 @@ static size_t wots_sign(slh_var_t *var, uint8_t *sig, const uint8_t *m)
   wots_csum(vm, m, prm);
 
   for (i = 0; i < len; i++)
+  __loop__(
+    assigns(i, sig)
+    invariant(i <= len)
+    invariant(sig == loop_entry(sig) + i * n)
+  )
   {
     adrs_set_chain_address(var, i);
     prm->wots_chain(var, sig, vm[i]);
diff --git a/slh_var.h b/slh_var.h
index 3be27a4..18acace 100644
--- a/slh_var.h
+++ b/slh_var.h
@@ -57,5 +57,13 @@ struct slh_var_s
 /* Core signing function (of a randomized digest) with initialized context. */
 size_t slh_do_sign(slh_var_t *var, uint8_t *sig, const uint8_t *digest);
 
+
+/* TODO: find a better place where to put the contract*/
+void wots_chain_contract(slh_var_t *var, uint8_t *tmp, uint32_t s)
+__contract__(
+  requires(memory_no_alias(var, sizeof(slh_var_t)))
+);
+
+
 /* _SLH_VAR_H_ */
 #endif