diff --git a/source/core_json.c b/source/core_json.c
index a01c393..ad48f28 100644
--- a/source/core_json.c
+++ b/source/core_json.c
@@ -63,6 +63,21 @@ typedef union
 #define isCurlyOpen_( x )             ( ( x ) == '{' )
 #define isCurlyClose_( x )            ( ( x ) == '}' )
 
+/**
+ * Renaming all loop-contract clauses from CBMC for readability.
+ * For more information about loop contracts in CBMC, see
+ * https://diffblue.github.io/cbmc/contracts-user.html.
+ */
+#ifdef CBMC
+    #define loopInvariant(...)       __CPROVER_loop_invariant(__VA_ARGS__)
+    #define decreases(...)           __CPROVER_decreases(__VA_ARGS__)
+    #define assigns(...)             __CPROVER_assigns(__VA_ARGS__)
+#else
+    #define loopInvariant(...)
+    #define decreases(...)
+    #define assigns(...)
+#endif
+
 /**
  * @brief Advance buffer index beyond whitespace.
  *
@@ -79,6 +94,9 @@ static void skipSpace( const char * buf,
     coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
     for( i = *start; i < max; i++ )
+    assigns( i )
+    loopInvariant( *start <= i && i <= max )
+    decreases( max - i )
     {
         if( !isspace_( buf[ i ] ) )
         {
@@ -103,6 +121,13 @@ static size_t countHighBits( uint8_t c )
     size_t i = 0;
 
     while( ( n & 0x80U ) != 0U )
+    assigns( i, n )
+    loopInvariant (
+        ( 0U <= i ) && ( i <= 8U )
+        && ( n == ( c & ( 0xFF >> i ) ) << i )
+        && ( ( ( c >> ( 8U - i ) ) + 1U ) == ( 1U << i ) )
+    )
+    decreases( 8U - i )
     {
         i++;
         n = ( n & 0x7FU ) << 1U;
@@ -211,6 +236,13 @@ static bool skipUTF8MultiByte( const char * buf,
         /* The bit count is 1 greater than the number of bytes,
          * e.g., when j is 2, we skip one more byte. */
         for( j = bitCount - 1U; j > 0U; j-- )
+        assigns( j, i, value, c.c )
+        loopInvariant(
+            ( 0 <= j ) && ( j <= bitCount - 1 )
+            && ( *start <= i ) && ( i <= max )
+            && ( ( i == max ) ==> ( j > 0 ) )
+        )
+        decreases( j )
         {
             i++;
 
@@ -343,6 +375,12 @@ static bool skipOneHexEscape( const char * buf,
     if( ( end > i ) && ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) )
     {
         for( i += 2U; i < end; i++ )
+        assigns( value, i )
+        loopInvariant(
+            ( *start + 2U <= i ) && ( i <= end ) &&
+            ( 0U <= value ) && ( value < ( 1U << ( 4U * ( i - ( 2U + *start ) ) ) ) )
+        )
+        decreases( end - i )
         {
             uint8_t n = hexToInt( buf[ i ] );
 
@@ -505,6 +543,9 @@ static bool skipString( const char * buf,
         i++;
 
         while( i < max )
+        assigns( i )
+        loopInvariant( *start + 1U <= i && i <= max )
+        decreases( max - i )
         {
             if( buf[ i ] == '"' )
             {
@@ -563,6 +604,9 @@ static bool strnEq( const char * a,
     coreJSON_ASSERT( ( a != NULL ) && ( b != NULL ) );
 
     for( i = 0; i < n; i++ )
+    assigns( i )
+    loopInvariant( i <= n )
+    decreases( n - i )
     {
         if( a[ i ] != b[ i ] )
         {
@@ -678,6 +722,9 @@ static bool skipDigits( const char * buf,
     saveStart = *start;
 
     for( i = *start; i < max; i++ )
+    assigns( value, i )
+    loopInvariant( *start <= i && i <= max )
+    decreases( max - i )
     {
         if( !isdigit_( buf[ i ] ) )
         {
@@ -928,6 +975,9 @@ static bool skipArrayScalars( const char * buf,
     i = *start;
 
     while( i < max )
+    assigns( i )
+    loopInvariant( *start <= i && i <= max )
+    decreases( max - i )
     {
         if( skipAnyScalar( buf, &i, max ) != true )
         {
@@ -982,6 +1032,13 @@ static bool skipObjectScalars( const char * buf,
     i = *start;
 
     while( i < max )
+    assigns( i, *start, comma )
+    loopInvariant(
+        i >= *start
+        && __CPROVER_loop_entry( i ) <= i && i <= max
+        && __CPROVER_loop_entry( *start ) <= *start && *start <= max
+    )
+    decreases( max - i )
     {
         if( skipString( buf, &i, max ) != true )
         {
@@ -1109,6 +1166,14 @@ static JSONStatus_t skipCollection( const char * buf,
     i = *start;
 
     while( i < max )
+    assigns( i, depth, c, ret, __CPROVER_object_whole( stack ) )
+    loopInvariant(
+        -1 <= depth && depth <= JSON_MAX_DEPTH
+        && *start <= i && i <= max
+        && ( ( ret == JSONSuccess ) ==> i >= *start + 2U )
+        && ( ret == JSONSuccess || ret == JSONPartial || ret == JSONIllegalDocument || ret == JSONMaxDepthExceeded )
+    )
+    decreases( max - i )
     {
         c = buf[ i ];
         i++;
@@ -1144,6 +1209,7 @@ static JSONStatus_t skipCollection( const char * buf,
 
                     if( skipSpaceAndComma( buf, &i, max ) == true )
                     {
+                        __CPROVER_assume( isOpenBracket_(stack[depth]));
                         if( skipScalars( buf, &i, max, stack[ depth ] ) != true )
                         {
                             ret = JSONIllegalDocument;
@@ -1406,6 +1472,9 @@ static bool objectSearch( const char * buf,
         skipSpace( buf, &i, max );
 
         while( i < max )
+        assigns( i, key, keyLength, value, valueLength )
+        loopInvariant( __CPROVER_loop_entry( i ) <= i && i <= max )
+        decreases( max - i )
         {
             if( nextKeyValuePair( buf, &i, max, &key, &keyLength,
                                   &value, &valueLength ) != true )
@@ -1473,6 +1542,9 @@ static bool arraySearch( const char * buf,
         skipSpace( buf, &i, max );
 
         while( i < max )
+        assigns( i, currentIndex, value, valueLength )
+        loopInvariant( __CPROVER_loop_entry( i ) <= i && i <= max && currentIndex < i )
+        decreases( max - i )
         {
             if( nextValue( buf, &i, max, &value, &valueLength ) != true )
             {
@@ -1538,6 +1610,9 @@ static bool skipQueryPart( const char * buf,
     while( ( i < max ) &&
            !isSeparator_( buf[ i ] ) &&
            !isSquareOpen_( buf[ i ] ) )
+    assigns( i )
+    loopInvariant( i  <= max )
+    decreases( max - i )
     {
         i++;
     }
@@ -1584,6 +1659,17 @@ static JSONStatus_t multiSearch( const char * buf,
     coreJSON_ASSERT( ( max > 0U ) && ( queryLength > 0U ) );
 
     while( i < queryLength )
+    assigns( i, start, queryStart, value, length )
+    loopInvariant(
+           0U <= start && start < max
+        && 0U < length && length <= max
+        && start + length <= max
+        && ( ( i == queryLength && ret == JSONSuccess && buf[ start ] == '"' ) ==> length >= 2U )
+        && 0U <= value && value < max
+        && 0U <= i && i <= queryLength
+        && 0U <= queryStart && queryStart <= queryLength
+    )
+    decreases( queryLength - i )
     {
         bool found = false;