diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index e39af014..df6032ba 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -161,3 +161,4 @@ jobs:
         uses: FreeRTOS/CI-CD-Github-Actions/run_cbmc@main
         with:
           proofs_dir: test/cbmc/proofs
+          run_cbmc_proofs_command: cd ../../../; git apply -v loop_invariants.patch; cd test/cbmc/proofs; ./run-cbmc-proofs.py
diff --git a/loop_invariants.patch b/loop_invariants.patch
new file mode 100644
index 00000000..f364b92e
--- /dev/null
+++ b/loop_invariants.patch
@@ -0,0 +1,202 @@
+diff --git a/source/core_json.c b/source/core_json.c
+index 901b2e1..8bdd89c 100644
+--- a/source/core_json.c
++++ b/source/core_json.c
+@@ -62,6 +62,21 @@ typedef union
+ #define isSquareOpen_( x )            ( ( x ) == '[' )
+ #define isSquareClose_( 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.
+  *
+@@ -78,6 +93,9 @@ static void skipSpace( const char * buf,
+     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 ] ) )
+         {
+@@ -102,6 +120,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;
+@@ -210,6 +235,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++;
+ 
+@@ -345,6 +377,12 @@ static bool skipOneHexEscape( const char * buf,
+     if( ( 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 ] );
+ 
+@@ -522,6 +560,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 ] == '"' )
+             {
+@@ -580,6 +621,9 @@ static bool strnEq( const char * a,
+     assert( ( a != NULL ) && ( b != NULL ) );
+ 
+     for( i = 0; i < n; i++ )
++    assigns( i )
++    loopInvariant( i <= n )
++    decreases( n - i )
+     {
+         if( a[ i ] != b[ i ] )
+         {
+@@ -681,6 +725,7 @@ static bool skipAnyLiteral( const char * buf,
+  * false otherwise.
+  */
+ #define MAX_FACTOR    ( MAX_INDEX_VALUE / 10 )
++
+ static bool skipDigits( const char * buf,
+                         size_t * start,
+                         size_t max,
+@@ -695,6 +740,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 ] ) )
+         {
+@@ -944,6 +992,9 @@ static void 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 )
+         {
+@@ -986,6 +1037,13 @@ static void 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 )
+         {
+@@ -1082,6 +1140,14 @@ static JSONStatus_t skipCollection( const char * buf,
+     i = *start;
+ 
+     while( i < max )
++    assigns( i, depth, c, __CPROVER_object_whole( stack ), ret )
++    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++;
+@@ -1363,6 +1429,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 )
+@@ -1430,6 +1499,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 )
+             {
+@@ -1495,6 +1567,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++;
+     }
+@@ -1541,6 +1616,17 @@ static JSONStatus_t multiSearch( const char * buf,
+     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;
+ 
diff --git a/source/core_json.c b/source/core_json.c
index 928bb02a..901b2e16 100644
--- a/source/core_json.c
+++ b/source/core_json.c
@@ -73,7 +73,7 @@ static void skipSpace( const char * buf,
                        size_t * start,
                        size_t max )
 {
-    size_t i;
+    size_t i = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -131,7 +131,7 @@ static bool shortestUTF8( size_t length,
                           uint32_t value )
 {
     bool ret = false;
-    uint32_t min, max;
+    uint32_t min = 0U, max = 0U;
 
     assert( ( length >= 2U ) && ( length <= 4U ) );
 
@@ -190,9 +190,9 @@ static bool skipUTF8MultiByte( const char * buf,
                                size_t max )
 {
     bool ret = false;
-    size_t i, bitCount, j;
-    uint32_t value = 0;
-    char_ c;
+    size_t i = 0U, bitCount = 0U, j = 0U;
+    uint32_t value = 0U;
+    char_ c = { 0 };
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -283,7 +283,7 @@ static bool skipUTF8( const char * buf,
 #define NOT_A_HEX_CHAR    ( 0x10U )
 static uint8_t hexToInt( char c )
 {
-    char_ n;
+    char_ n = { 0 };
 
     n.c = c;
 
@@ -329,8 +329,8 @@ static bool skipOneHexEscape( const char * buf,
                               uint16_t * outValue )
 {
     bool ret = false;
-    size_t i, end;
-    uint16_t value = 0;
+    size_t i = 0U, end = 0U;
+    uint16_t value = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
     assert( outValue != NULL );
@@ -392,8 +392,8 @@ static bool skipHexEscape( const char * buf,
                            size_t max )
 {
     bool ret = false;
-    size_t i;
-    uint16_t value;
+    size_t i = 0U;
+    uint16_t value = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -444,7 +444,7 @@ static bool skipEscape( const char * buf,
                         size_t max )
 {
     bool ret = false;
-    size_t i;
+    size_t i = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -511,7 +511,7 @@ static bool skipString( const char * buf,
                         size_t max )
 {
     bool ret = false;
-    size_t i;
+    size_t i = 0;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -575,7 +575,7 @@ static bool strnEq( const char * a,
                     const char * b,
                     size_t n )
 {
-    size_t i;
+    size_t i = 0U;
 
     assert( ( a != NULL ) && ( b != NULL ) );
 
@@ -640,7 +640,7 @@ static bool skipAnyLiteral( const char * buf,
                             size_t * start,
                             size_t max )
 {
-    bool ret;
+    bool ret = false;
 
 #define skipLit_( x ) \
     ( skipLiteral( buf, start, max, ( x ), ( sizeof( x ) - 1UL ) ) == true )
@@ -687,8 +687,8 @@ static bool skipDigits( const char * buf,
                         int32_t * outValue )
 {
     bool ret = false;
-    size_t i, saveStart;
-    int32_t value = 0;
+    size_t i = 0U, saveStart = 0U;
+    int32_t value = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -741,7 +741,7 @@ static void skipDecimals( const char * buf,
                           size_t * start,
                           size_t max )
 {
-    size_t i;
+    size_t i = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -769,7 +769,7 @@ static void skipExponent( const char * buf,
                           size_t * start,
                           size_t max )
 {
-    size_t i;
+    size_t i = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -806,7 +806,7 @@ static bool skipNumber( const char * buf,
                         size_t max )
 {
     bool ret = false;
-    size_t i;
+    size_t i = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -861,7 +861,7 @@ static bool skipAnyScalar( const char * buf,
                            size_t * start,
                            size_t max )
 {
-    bool ret;
+    bool ret = false;
 
     if( skipString( buf, start, max ) == true )
     {
@@ -902,7 +902,7 @@ static bool skipSpaceAndComma( const char * buf,
                                size_t max )
 {
     bool ret = false;
-    size_t i;
+    size_t i = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -937,7 +937,7 @@ static void skipArrayScalars( const char * buf,
                               size_t * start,
                               size_t max )
 {
-    size_t i;
+    size_t i = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -978,8 +978,8 @@ static void skipObjectScalars( const char * buf,
                                size_t * start,
                                size_t max )
 {
-    size_t i;
-    bool comma;
+    size_t i = 0U;
+    bool comma = false;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -1075,7 +1075,7 @@ static JSONStatus_t skipCollection( const char * buf,
     JSONStatus_t ret = JSONPartial;
     char c, stack[ JSON_MAX_DEPTH ];
     int16_t depth = -1;
-    size_t i;
+    size_t i = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -1092,7 +1092,7 @@ static JSONStatus_t skipCollection( const char * buf,
             case '[':
                 depth++;
 
-                if( depth == JSON_MAX_DEPTH )
+                if( depth >= JSON_MAX_DEPTH )
                 {
                     ret = JSONMaxDepthExceeded;
                     break;
@@ -1105,11 +1105,13 @@ static JSONStatus_t skipCollection( const char * buf,
             case '}':
             case ']':
 
-                if( ( depth > 0 ) && isMatchingBracket_( stack[ depth ], c ) )
+                if( ( depth > 0 ) && ( depth < JSON_MAX_DEPTH ) &&
+                    isMatchingBracket_( stack[ depth ], c ) )
                 {
                     depth--;
 
-                    if( skipSpaceAndComma( buf, &i, max ) == true )
+                    if( ( skipSpaceAndComma( buf, &i, max ) == true ) &&
+                        isOpenBracket_( stack[ depth ] ) )
                     {
                         skipScalars( buf, &i, max, stack[ depth ] );
                     }
@@ -1152,7 +1154,7 @@ JSONStatus_t JSON_Validate( const char * buf,
                             size_t max )
 {
     JSONStatus_t ret;
-    size_t i = 0;
+    size_t i = 0U;
 
     if( buf == NULL )
     {
@@ -1218,7 +1220,7 @@ static bool nextValue( const char * buf,
                        size_t * valueLength )
 {
     bool ret = true;
-    size_t i, valueStart;
+    size_t i = 0U, valueStart = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
     assert( ( value != NULL ) && ( valueLength != NULL ) );
@@ -1275,7 +1277,7 @@ static bool nextKeyValuePair( const char * buf,
                               size_t * valueLength )
 {
     bool ret = true;
-    size_t i, keyStart;
+    size_t i = 0U, keyStart = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
     assert( ( key != NULL ) && ( keyLength != NULL ) );
@@ -1348,7 +1350,7 @@ static bool objectSearch( const char * buf,
 {
     bool ret = false;
 
-    size_t i = 0, key, keyLength, value = 0, valueLength = 0;
+    size_t i = 0U, key = 0U, keyLength = 0U, value = 0U, valueLength = 0U;
 
     assert( ( buf != NULL ) && ( query != NULL ) );
     assert( ( outValue != NULL ) && ( outValueLength != NULL ) );
@@ -1414,8 +1416,8 @@ static bool arraySearch( const char * buf,
                          size_t * outValueLength )
 {
     bool ret = false;
-    size_t i = 0, value = 0, valueLength = 0;
-    uint32_t currentIndex = 0;
+    size_t i = 0U, value = 0U, valueLength = 0U;
+    uint32_t currentIndex = 0U;
 
     assert( buf != NULL );
     assert( ( outValue != NULL ) && ( outValueLength != NULL ) );
@@ -1440,7 +1442,8 @@ static bool arraySearch( const char * buf,
                 break;
             }
 
-            if( skipSpaceAndComma( buf, &i, max ) != true )
+            if( ( skipSpaceAndComma( buf, &i, max ) != true ) ||
+                ( currentIndex == UINT32_MAX ) )
             {
                 break;
             }
@@ -1482,7 +1485,7 @@ static bool skipQueryPart( const char * buf,
                            size_t * outLength )
 {
     bool ret = false;
-    size_t i;
+    size_t i = 0U;
 
     assert( ( buf != NULL ) && ( start != NULL ) && ( outLength != NULL ) );
     assert( max > 0U );
@@ -1531,7 +1534,7 @@ static JSONStatus_t multiSearch( const char * buf,
                                  size_t * outValueLength )
 {
     JSONStatus_t ret = JSONSuccess;
-    size_t i = 0, start = 0, queryStart = 0, value = 0, length = max;
+    size_t i = 0U, start = 0U, queryStart = 0U, value = 0U, length = max;
 
     assert( ( buf != NULL ) && ( query != NULL ) );
     assert( ( outValue != NULL ) && ( outValueLength != NULL ) );
@@ -1797,7 +1800,7 @@ JSONStatus_t JSON_Iterate( const char * buf,
                            JSONPair_t * outPair )
 {
     JSONStatus_t ret;
-    size_t key, keyLength, value, valueLength;
+    size_t key = 0U, keyLength = 0U, value = 0U, valueLength = 0U;
 
     if( ( buf == NULL ) || ( start == NULL ) || ( next == NULL ) ||
         ( outPair == NULL ) )
diff --git a/test/cbmc/include/core_json_contracts.h b/test/cbmc/include/core_json_contracts.h
index 1f0936f2..fec38860 100644
--- a/test/cbmc/include/core_json_contracts.h
+++ b/test/cbmc/include/core_json_contracts.h
@@ -87,80 +87,93 @@
  * These are declarations for all predicates used in coreJSON function contracts.
  */
 
-bool isValidBoundedBuffer( char * buf,
-                           size_t max );
-bool isValidBoundedBufferWithStartIndex( char * buf,
-                                         size_t max,
-                                         size_t * start );
+bool isValidBuffer( const char * buf,
+                    size_t max );
+bool isValidBufferWithStartIndex( const char * buf,
+                                  size_t max,
+                                  size_t * start );
 bool isValidStart( size_t start,
                    size_t old_start,
                    size_t max );
-bool JSON_SearchConstPreconditions( char * buf,
+bool JSON_SearchConstPreconditions( const char * buf,
                                     size_t max,
-                                    char * query,
+                                    const char * query,
                                     size_t queryLength,
-                                    char ** outValue,
+                                    const char ** outValue,
                                     size_t * outValueLength,
                                     JSONTypes_t * outType );
 bool JSON_SearchConstPostconditions( JSONStatus_t result,
-                                     char * buf,
-                                     char ** outValue,
+                                     const char * buf,
+                                     const char ** outValue,
                                      size_t * outValueLength,
                                      size_t max );
-bool JSON_IteratePreconditions( char * buf,
+bool JSON_IteratePreconditions( const char * buf,
                                 size_t max,
                                 size_t * start,
                                 size_t * next,
                                 JSONPair_t * outPair );
 bool JSON_IteratePostconditions( JSONStatus_t result,
-                                 char * buf,
+                                 const char * buf,
                                  size_t max,
                                  JSONPair_t * outPair );
-JSONStatus_t JSON_ValidatePreconditions( char * buf,
+JSONStatus_t JSON_ValidatePreconditions( const char * buf,
                                          size_t max );
-bool arraySearchPreconditions( char * buf,
+bool arraySearchPreconditions( const char * buf,
                                size_t max,
                                size_t * outValue,
                                size_t * outValueLength );
 bool arraySearchPostconditions( bool result,
-                                char * buf,
+                                const char * buf,
                                 size_t max,
                                 size_t * outValue,
                                 size_t * outValueLength,
                                 size_t old_outValue,
                                 size_t old_outValueLength );
-bool objectSearchPreconditions( char * buf,
+bool objectSearchPreconditions( const char * buf,
                                 size_t max,
                                 const char * query,
                                 size_t queryLength,
                                 size_t * outValue,
                                 size_t * outValueLength );
+bool multiSearchPreconditions( const char * buf,
+                               size_t max,
+                               const char * query,
+                               size_t queryLength,
+                               size_t * outValue,
+                               size_t * outValueLength );
+bool multiSearchPostconditions( JSONStatus_t result,
+                                const char * buf,
+                                size_t max,
+                                size_t * outValue,
+                                size_t * outValueLength,
+                                size_t old_outValue,
+                                size_t old_outValueLength );
 bool skipPostconditions( bool result,
-                         char * buf,
+                         const char * buf,
                          size_t * start,
                          size_t old_start,
                          size_t max,
                          size_t gap );
 bool skipCollectionPostconditions( JSONStatus_t result,
-                                   char * buf,
+                                   const char * buf,
                                    size_t * start,
                                    size_t old_start,
                                    size_t max );
-bool skipScalarsPreconditions( char * buf,
+bool skipScalarsPreconditions( const char * buf,
                                size_t * start,
                                size_t max,
                                char mode );
 bool skipAnyScalarPostconditions( bool result,
-                                  char * buf,
+                                  const char * buf,
                                   size_t * start,
                                   size_t old_start,
                                   size_t max );
-bool skipDigitsPreconditions( char * buf,
+bool skipDigitsPreconditions( const char * buf,
                               size_t * start,
                               size_t max,
                               int32_t * outValue );
 bool skipDigitsPostconditions( bool result,
-                               char * buf,
+                               const char * buf,
                                size_t * start,
                                size_t old_start,
                                size_t max,
@@ -229,10 +242,21 @@ assigns( *outValue, *outValueLength )
 ensures( arraySearchPostconditions( result, buf, max, outValue, outValueLength, old( *outValue ), old( *outValueLength ) ) )
 ;
 
+JSONStatus_t multiSearch( const char * buf,
+                          size_t max,
+                          const char * query,
+                          size_t queryLength,
+                          size_t * outValue,
+                          size_t * outValueLength )
+requires( multiSearchPreconditions( buf, max, query, queryLength, outValue, outValueLength ) )
+assigns( *outValue, *outValueLength )
+ensures( multiSearchPostconditions( result, buf, max, outValue, outValueLength, old( *outValue ), old( *outValueLength ) ) )
+;
+
 JSONStatus_t skipCollection( const char * buf,
                              size_t * start,
                              size_t max )
-requires( isValidBoundedBufferWithStartIndex( buf, max, start ) )
+requires( isValidBufferWithStartIndex( buf, max, start ) )
 assigns( *start )
 ensures( skipCollectionPostconditions( result, buf, start, old( *start ), max ) )
 ;
@@ -249,7 +273,7 @@ ensures( isValidStart( *start, old( *start ), max ) )
 void skipObjectScalars( const char * buf,
                         size_t * start,
                         size_t max )
-requires( isValidBoundedBufferWithStartIndex( buf, max, start ) )
+requires( isValidBufferWithStartIndex( buf, max, start ) )
 assigns( *start )
 ensures( isValidStart( *start, old( *start ), max ) )
 ;
@@ -257,7 +281,7 @@ ensures( isValidStart( *start, old( *start ), max ) )
 bool skipAnyScalar( const char * buf,
                     size_t * start,
                     size_t max )
-requires( isValidBoundedBufferWithStartIndex( buf, max, start ) )
+requires( isValidBufferWithStartIndex( buf, max, start ) )
 assigns( *start )
 ensures( skipAnyScalarPostconditions( result, buf, start, old( *start ), max ) )
 ;
@@ -265,7 +289,7 @@ ensures( skipAnyScalarPostconditions( result, buf, start, old( *start ), max ) )
 void skipSpace( const char * buf,
                 size_t * start,
                 size_t max )
-requires( isValidBoundedBufferWithStartIndex( buf, max, start ) )
+requires( isValidBufferWithStartIndex( buf, max, start ) )
 assigns( *start )
 ensures( isValidStart( *start, old( *start ), max ) )
 ;
@@ -273,7 +297,7 @@ ensures( isValidStart( *start, old( *start ), max ) )
 bool skipString( const char * buf,
                  size_t * start,
                  size_t max )
-requires( isValidBoundedBufferWithStartIndex( buf, max, start ) )
+requires( isValidBufferWithStartIndex( buf, max, start ) )
 assigns( *start )
 ensures( skipPostconditions( result, buf, start, old( *start ), max, 1 ) )
 ;
@@ -281,7 +305,7 @@ ensures( skipPostconditions( result, buf, start, old( *start ), max, 1 ) )
 bool skipEscape( const char * buf,
                  size_t * start,
                  size_t max )
-requires( isValidBoundedBufferWithStartIndex( buf, max, start ) )
+requires( isValidBufferWithStartIndex( buf, max, start ) )
 assigns( *start )
 ensures( skipPostconditions( result, buf, start, old( *start ), max, 1 ) )
 ;
@@ -289,7 +313,7 @@ ensures( skipPostconditions( result, buf, start, old( *start ), max, 1 ) )
 bool skipUTF8( const char * buf,
                size_t * start,
                size_t max )
-requires( isValidBoundedBufferWithStartIndex( buf, max, start ) )
+requires( isValidBufferWithStartIndex( buf, max, start ) )
 assigns( *start )
 ensures( skipPostconditions( result, buf, start, old( *start ), max, 0 ) )
 ;
diff --git a/test/cbmc/proofs/JSON_Iterate/Makefile b/test/cbmc/proofs/JSON_Iterate/Makefile
index 41e87175..ec4d2297 100644
--- a/test/cbmc/proofs/JSON_Iterate/Makefile
+++ b/test/cbmc/proofs/JSON_Iterate/Makefile
@@ -5,19 +5,14 @@ PROOF_UID=JSON_Iterate
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
 CBMC_OBJECT_BITS = 12
 
-UNWINDSET += JSON_Iterate.0:$(CBMC_MAX_BUFSIZE)
-
 USE_FUNCTION_CONTRACTS += skipAnyScalar
 USE_FUNCTION_CONTRACTS += skipCollection
 USE_FUNCTION_CONTRACTS += skipSpace
 USE_FUNCTION_CONTRACTS += skipString
 
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/JSON_SearchConst/Makefile b/test/cbmc/proofs/JSON_SearchConst/Makefile
index 7d11d945..dcefe78d 100644
--- a/test/cbmc/proofs/JSON_SearchConst/Makefile
+++ b/test/cbmc/proofs/JSON_SearchConst/Makefile
@@ -5,25 +5,13 @@ PROOF_UID=JSON_SearchConst
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
 CBMC_OBJECT_BITS = 11
 
-UNWINDSET += multiSearch.0:$(CBMC_MAX_QUERYKEYLENGTH)
-UNWINDSET += skipQueryPart.0:$(CBMC_MAX_QUERYKEYLENGTH)
+USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver kissat
 
-USE_FUNCTION_CONTRACTS += arraySearch
-USE_FUNCTION_CONTRACTS += objectSearch
-USE_FUNCTION_CONTRACTS += skipAnyScalar
-USE_FUNCTION_CONTRACTS += skipCollection
-USE_FUNCTION_CONTRACTS += skipDigits
-USE_FUNCTION_CONTRACTS += skipSpace
-USE_FUNCTION_CONTRACTS += skipString
-
-USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical
+USE_FUNCTION_CONTRACTS += multiSearch
 
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/JSON_Validate/Makefile b/test/cbmc/proofs/JSON_Validate/Makefile
index 1c7ad6b3..9bbf9bc1 100644
--- a/test/cbmc/proofs/JSON_Validate/Makefile
+++ b/test/cbmc/proofs/JSON_Validate/Makefile
@@ -1,23 +1,16 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: MIT-0
 
-EXPENSIVE = true
-
 PROOF_UID=JSON_Validate
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
-UNWINDSET += skipSpace.0:$(CBMC_MAX_BUFSIZE)
+USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical
 
 USE_FUNCTION_CONTRACTS += skipAnyScalar
 USE_FUNCTION_CONTRACTS += skipCollection
 
-USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical
-
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/Makefile-json.common b/test/cbmc/proofs/Makefile-json.common
index 22d3b60b..cce13279 100644
--- a/test/cbmc/proofs/Makefile-json.common
+++ b/test/cbmc/proofs/Makefile-json.common
@@ -3,16 +3,6 @@
 
 HARNESS_ENTRY=harness
 
-# This value was experimentally chosen to provide 100% coverage
-# without tripping unwinding assertions and without exhausting memory.
-CBMC_MAX_BUFSIZE ?= 11
-CBMC_MAX_QUERYKEYLENGTH ?= 6
-
-DEFINES += -DCBMC_MAX_BUFSIZE=$(CBMC_MAX_BUFSIZE)
-ifdef CBMC_MAX_QUERYKEYLENGTH
-    DEFINES += -DCBMC_MAX_QUERYKEYLENGTH=$(CBMC_MAX_QUERYKEYLENGTH)
-endif
-
 INCLUDES += -I$(CBMC_ROOT)/include
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
@@ -28,3 +18,7 @@ include ../Makefile.common
 
 cleanclean: veryclean
 	-$(RM) $(PROOFDIR)/core_json.c
+
+# Substitution command to pass to sed for patching core_json.c. The
+# characters " and # must be escaped with backslash.
+CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/arraySearch/Makefile b/test/cbmc/proofs/arraySearch/Makefile
index dc58e375..e5f31ae7 100644
--- a/test/cbmc/proofs/arraySearch/Makefile
+++ b/test/cbmc/proofs/arraySearch/Makefile
@@ -5,19 +5,13 @@ PROOF_UID=arraySearch
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
 CBMC_OBJECT_BITS = 12
 
-UNWINDSET += arraySearch.0:$(CBMC_MAX_BUFSIZE)
-UNWINDSET += arraySearch.1:$(CBMC_MAX_BUFSIZE)
-
 USE_FUNCTION_CONTRACTS += skipAnyScalar
 USE_FUNCTION_CONTRACTS += skipCollection
 USE_FUNCTION_CONTRACTS += skipSpace
 
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/multiSearch/Makefile b/test/cbmc/proofs/multiSearch/Makefile
new file mode 100644
index 00000000..63d7ae23
--- /dev/null
+++ b/test/cbmc/proofs/multiSearch/Makefile
@@ -0,0 +1,19 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: MIT-0
+
+PROOF_UID=multiSearch
+CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
+HARNESS_FILE= $(PROOF_UID)_harness
+
+APPLY_LOOP_CONTRACTS = 1
+USE_DYNAMIC_FRAMES = 1
+
+CBMC_OBJECT_BITS = 12
+
+USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver kissat
+
+USE_FUNCTION_CONTRACTS += arraySearch
+USE_FUNCTION_CONTRACTS += objectSearch
+USE_FUNCTION_CONTRACTS += skipDigits
+
+include ../Makefile-json.common
diff --git a/test/cbmc/proofs/multiSearch/README.md b/test/cbmc/proofs/multiSearch/README.md
new file mode 100644
index 00000000..44de39eb
--- /dev/null
+++ b/test/cbmc/proofs/multiSearch/README.md
@@ -0,0 +1,17 @@
+multiSearch proof
+==============
+
+This directory contains a memory safety proof for `multiSearch`.
+The proof runs in a few seconds and provides 100% coverage.
+
+For this proof, the following functions are replaced with function contracts.
+These functions have separate proofs.
+* `arraySearch`;
+* `objectSearch`;
+* `skipDigits`.
+
+To run the proof.
+* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer`
+  to your path;
+* Run `make`;
+* Open `html/index.html` in a web browser.
diff --git a/test/cbmc/proofs/multiSearch/cbmc-proof.txt b/test/cbmc/proofs/multiSearch/cbmc-proof.txt
new file mode 100644
index 00000000..6ed46f12
--- /dev/null
+++ b/test/cbmc/proofs/multiSearch/cbmc-proof.txt
@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.
diff --git a/test/cbmc/proofs/multiSearch/cbmc-viewer.json b/test/cbmc/proofs/multiSearch/cbmc-viewer.json
new file mode 100644
index 00000000..e0fc0c4e
--- /dev/null
+++ b/test/cbmc/proofs/multiSearch/cbmc-viewer.json
@@ -0,0 +1,7 @@
+{ "expected-missing-functions":
+  [
+
+  ],
+  "proof-name": "multiSearch",
+  "proof-root": "test/cbmc/proofs"
+}
diff --git a/test/cbmc/proofs/multiSearch/multiSearch_harness.c b/test/cbmc/proofs/multiSearch/multiSearch_harness.c
new file mode 100644
index 00000000..07b932ab
--- /dev/null
+++ b/test/cbmc/proofs/multiSearch/multiSearch_harness.c
@@ -0,0 +1,42 @@
+/*
+ * coreJSON v3.2.0
+ * Copyright (C) 2020 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * SPDX-License-Identifier: MIT
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+/**
+ * @file multiSearch_harness.c
+ * @brief Implements the proof harness for the multiSearch function.
+ */
+
+#include "core_json_contracts.h"
+
+void harness()
+{
+    char * buf;
+    size_t max;
+    char * query;
+    size_t queryLength;
+    char * outValue;
+    size_t * outValueLength;
+
+    multiSearch( buf, max, query, queryLength, outValue, outValueLength );
+}
diff --git a/test/cbmc/proofs/objectSearch/Makefile b/test/cbmc/proofs/objectSearch/Makefile
index fab42f11..c0af4caf 100644
--- a/test/cbmc/proofs/objectSearch/Makefile
+++ b/test/cbmc/proofs/objectSearch/Makefile
@@ -1,28 +1,20 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: MIT-0
 
-EXPENSIVE = true
-
 PROOF_UID=objectSearch
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
 CBMC_OBJECT_BITS = 11
 
-UNWINDSET += objectSearch.0:$(CBMC_MAX_BUFSIZE)
-UNWINDSET += strnEq.0:$(CBMC_MAX_BUFSIZE)
+USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical
 
 USE_FUNCTION_CONTRACTS += skipAnyScalar
 USE_FUNCTION_CONTRACTS += skipCollection
 USE_FUNCTION_CONTRACTS += skipSpace
 USE_FUNCTION_CONTRACTS += skipString
 
-USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical
-
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/skipAnyScalar/Makefile b/test/cbmc/proofs/skipAnyScalar/Makefile
index 96b29a0e..ba922681 100644
--- a/test/cbmc/proofs/skipAnyScalar/Makefile
+++ b/test/cbmc/proofs/skipAnyScalar/Makefile
@@ -5,16 +5,10 @@ PROOF_UID=skipAnyScalar
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
-UNWINDSET += skipAnyScalar.0:$(CBMC_MAX_BUFSIZE)
-UNWINDSET += strnEq.0:$(CBMC_MAX_BUFSIZE)
-
 USE_FUNCTION_CONTRACTS += skipDigits
 USE_FUNCTION_CONTRACTS += skipString
 
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/skipCollection/Makefile b/test/cbmc/proofs/skipCollection/Makefile
index 17e7999d..de423826 100644
--- a/test/cbmc/proofs/skipCollection/Makefile
+++ b/test/cbmc/proofs/skipCollection/Makefile
@@ -5,19 +5,12 @@ PROOF_UID=skipCollection
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
 CBMC_OBJECT_BITS = 10
 
-DEFINES += -DJSON_MAX_DEPTH="( $(CBMC_MAX_BUFSIZE) - 2 )"
-
 USE_FUNCTION_CONTRACTS += skipScalars
 USE_FUNCTION_CONTRACTS += skipSpace
 
-UNWINDSET += skipCollection.0:$(CBMC_MAX_BUFSIZE)
-
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/skipDigits/Makefile b/test/cbmc/proofs/skipDigits/Makefile
index c0b33dff..657ddcbd 100644
--- a/test/cbmc/proofs/skipDigits/Makefile
+++ b/test/cbmc/proofs/skipDigits/Makefile
@@ -5,12 +5,7 @@ PROOF_UID=skipDigits
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
-UNWINDSET += skipDigits.0:$(CBMC_MAX_BUFSIZE)
-
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/skipEscape/Makefile b/test/cbmc/proofs/skipEscape/Makefile
index 0ba03f70..84518f98 100644
--- a/test/cbmc/proofs/skipEscape/Makefile
+++ b/test/cbmc/proofs/skipEscape/Makefile
@@ -5,12 +5,7 @@ PROOF_UID=skipEscape
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
-UNWINDSET += skipOneHexEscape.0:$(CBMC_MAX_BUFSIZE)
-
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/skipObjectScalars/Makefile b/test/cbmc/proofs/skipObjectScalars/Makefile
index b0e137f5..55d32608 100644
--- a/test/cbmc/proofs/skipObjectScalars/Makefile
+++ b/test/cbmc/proofs/skipObjectScalars/Makefile
@@ -1,26 +1,19 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: MIT-0
 
-EXPENSIVE = true
-
 PROOF_UID=skipObjectScalars
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
 CBMC_OBJECT_BITS = 11
 
-UNWINDSET += skipObjectScalars.0:$(CBMC_MAX_BUFSIZE)
+USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical
 
 USE_FUNCTION_CONTRACTS += skipSpace
 USE_FUNCTION_CONTRACTS += skipAnyScalar
 USE_FUNCTION_CONTRACTS += skipString
 
-USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical
-
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/skipScalars/Makefile b/test/cbmc/proofs/skipScalars/Makefile
index c97367be..b2de06a0 100644
--- a/test/cbmc/proofs/skipScalars/Makefile
+++ b/test/cbmc/proofs/skipScalars/Makefile
@@ -5,21 +5,16 @@ PROOF_UID=skipScalars
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
 CBMC_OBJECT_BITS = 11
 
-UNWINDSET += skipArrayScalars.0:$(CBMC_MAX_BUFSIZE)
+USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical
 
 USE_FUNCTION_CONTRACTS += skipAnyScalar
 USE_FUNCTION_CONTRACTS += skipObjectScalars
 USE_FUNCTION_CONTRACTS += skipSpace
 USE_FUNCTION_CONTRACTS += skipString
 
-USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical
-
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/skipSpace/Makefile b/test/cbmc/proofs/skipSpace/Makefile
index 96c26bf3..3c6dc0ef 100644
--- a/test/cbmc/proofs/skipSpace/Makefile
+++ b/test/cbmc/proofs/skipSpace/Makefile
@@ -5,12 +5,7 @@ PROOF_UID=skipSpace
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
-UNWINDSET += skipSpace.0:$(CBMC_MAX_BUFSIZE)
-
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/skipString/Makefile b/test/cbmc/proofs/skipString/Makefile
index 50abf69e..8958116a 100644
--- a/test/cbmc/proofs/skipString/Makefile
+++ b/test/cbmc/proofs/skipString/Makefile
@@ -5,19 +5,14 @@ PROOF_UID=skipString
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
 CBMC_OBJECT_BITS = 10
 
 USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical
 
-UNWINDSET += skipString.0:$(CBMC_MAX_BUFSIZE)
-
 USE_FUNCTION_CONTRACTS += skipEscape
 USE_FUNCTION_CONTRACTS += skipUTF8
 
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/proofs/skipUTF8/Makefile b/test/cbmc/proofs/skipUTF8/Makefile
index 6c5c769d..a712a1cd 100644
--- a/test/cbmc/proofs/skipUTF8/Makefile
+++ b/test/cbmc/proofs/skipUTF8/Makefile
@@ -5,13 +5,7 @@ PROOF_UID=skipUTF8
 CHECK_FUNCTION_CONTRACTS = $(PROOF_UID)
 HARNESS_FILE= $(PROOF_UID)_harness
 
+APPLY_LOOP_CONTRACTS = 1
 USE_DYNAMIC_FRAMES = 1
 
-UNWINDSET += countHighBits.0:$(CBMC_MAX_BUFSIZE)
-UNWINDSET += skipUTF8MultiByte.0:$(CBMC_MAX_BUFSIZE)
-
 include ../Makefile-json.common
-
-# Substitution command to pass to sed for patching core_json.c. The
-# characters " and # must be escaped with backslash.
-CORE_JSON_SED_EXPR = s/^static //
diff --git a/test/cbmc/sources/core_json_contracts.c b/test/cbmc/sources/core_json_contracts.c
index 6fd2da3c..b4bb2bd7 100644
--- a/test/cbmc/sources/core_json_contracts.c
+++ b/test/cbmc/sources/core_json_contracts.c
@@ -36,19 +36,19 @@
  */
 
 /* Valid allocated buffer up to size max. */
-bool isValidBoundedBuffer( char * buf,
-                           size_t max )
+bool isValidBuffer( const char * buf,
+                    size_t max )
 {
-    return ( 0 < max && max < CBMC_MAX_BUFSIZE )
+    return ( 0U < max )
            & ( allocated( buf, max ) );
 }
 
 /* Valid allocated buffer up to size max and allocated start index. */
-bool isValidBoundedBufferWithStartIndex( char * buf,
-                                         size_t max,
-                                         size_t * start )
+bool isValidBufferWithStartIndex( const char * buf,
+                                  size_t max,
+                                  size_t * start )
 {
-    return isValidBoundedBuffer( buf, max )
+    return isValidBuffer( buf, max )
            & ( allocated( start, sizeof( *start ) ) );
 }
 
@@ -61,17 +61,15 @@ bool isValidStart( size_t start,
            ( ( old_start < max ) ? ( start <= max ) : ( start == old_start ) );
 }
 
-bool JSON_SearchConstPreconditions( char * buf,
+bool JSON_SearchConstPreconditions( const char * buf,
                                     size_t max,
-                                    char * query,
+                                    const char * query,
                                     size_t queryLength,
-                                    char ** outValue,
+                                    const char ** outValue,
                                     size_t * outValueLength,
                                     JSONTypes_t * outType )
 {
-    return ( max < CBMC_MAX_BUFSIZE )
-           & ( queryLength < CBMC_MAX_QUERYKEYLENGTH )
-           & ( buf == NULL || allocated( buf, max ) )
+    return ( buf == NULL || allocated( buf, max ) )
            & ( query == NULL || allocated( query, queryLength ) )
            & ( outValue == NULL || allocated( outValue, sizeof( *outValue ) ) )
            & ( outValueLength == NULL || allocated( outValueLength, sizeof( *outValueLength ) ) )
@@ -79,8 +77,8 @@ bool JSON_SearchConstPreconditions( char * buf,
 }
 
 bool JSON_SearchConstPostconditions( JSONStatus_t result,
-                                     char * buf,
-                                     char ** outValue,
+                                     const char * buf,
+                                     const char ** outValue,
                                      size_t * outValueLength,
                                      size_t max )
 {
@@ -96,13 +94,13 @@ bool JSON_SearchConstPostconditions( JSONStatus_t result,
     return validity;
 }
 
-bool JSON_IteratePreconditions( char * buf,
+bool JSON_IteratePreconditions( const char * buf,
                                 size_t max,
                                 size_t * start,
                                 size_t * next,
                                 JSONPair_t * outPair )
 {
-    return ( 0 < max && max < CBMC_MAX_BUFSIZE )
+    return ( 0 < max )
            & ( buf == NULL || allocated( buf, max ) )
            & ( start == NULL || allocated( start, sizeof( *start ) ) )
            & ( next == NULL || allocated( next, sizeof( *next ) ) )
@@ -112,7 +110,7 @@ bool JSON_IteratePreconditions( char * buf,
 }
 
 bool JSON_IteratePostconditions( JSONStatus_t result,
-                                 char * buf,
+                                 const char * buf,
                                  size_t max,
                                  JSONPair_t * outPair )
 {
@@ -129,26 +127,25 @@ bool JSON_IteratePostconditions( JSONStatus_t result,
     return validity;
 }
 
-JSONStatus_t JSON_ValidatePreconditions( char * buf,
+JSONStatus_t JSON_ValidatePreconditions( const char * buf,
                                          size_t max )
 {
-    return ( max < CBMC_MAX_BUFSIZE )
-           & ( buf == NULL || allocated( buf, max ) );
+    return( buf == NULL || allocated( buf, max ) );
 }
 
-bool arraySearchPreconditions( char * buf,
+bool arraySearchPreconditions( const char * buf,
                                size_t max,
                                size_t * outValue,
                                size_t * outValueLength )
 {
-    return ( isValidBoundedBuffer( buf, max ) )
+    return ( isValidBuffer( buf, max ) )
            & ( allocated( outValue, sizeof( *outValue ) ) )
            & ( allocated( outValueLength, sizeof( *outValueLength ) ) )
            & ( *outValueLength <= max );
 }
 
 bool arraySearchPostconditions( bool result,
-                                char * buf,
+                                const char * buf,
                                 size_t max,
                                 size_t * outValue,
                                 size_t * outValueLength,
@@ -159,7 +156,7 @@ bool arraySearchPostconditions( bool result,
 
     if( result )
     {
-        validity = ( 0 <= *outValue && *outValue < max ) &&
+        validity = ( *outValue < max ) &&
                    ( 0 < *outValueLength && *outValueLength <= max - *outValue ) &&
                    IMPLIES( buf[ *outValue ] == '"', ( 2 <= *outValueLength && *outValueLength <= max - *outValue ) );
     }
@@ -172,7 +169,7 @@ bool arraySearchPostconditions( bool result,
     return validity;
 }
 
-bool objectSearchPreconditions( char * buf,
+bool objectSearchPreconditions( const char * buf,
                                 size_t max,
                                 const char * query,
                                 size_t queryLength,
@@ -180,12 +177,39 @@ bool objectSearchPreconditions( char * buf,
                                 size_t * outValueLength )
 {
     return arraySearchPreconditions( buf, max, outValue, outValueLength )
-           & ( queryLength < CBMC_MAX_QUERYKEYLENGTH )
            & ( allocated( query, queryLength ) );
 }
 
+bool multiSearchPreconditions( const char * buf,
+                               size_t max,
+                               const char * query,
+                               size_t queryLength,
+                               size_t * outValue,
+                               size_t * outValueLength )
+{
+    return ( isValidBuffer( buf, max ) )
+           & ( 0U < queryLength )
+           & ( allocated( query, queryLength ) )
+           & ( allocated( outValue, sizeof( *outValue ) ) )
+           & ( allocated( outValueLength, sizeof( *outValueLength ) ) );
+}
+
+bool multiSearchPostconditions( JSONStatus_t result,
+                                const char * buf,
+                                size_t max,
+                                size_t * outValue,
+                                size_t * outValueLength,
+                                size_t old_outValue,
+                                size_t old_outValueLength )
+{
+    bool validity = isJSONSearchEnum( result ) &&
+                    arraySearchPostconditions( result == JSONSuccess, buf, max, outValue, outValueLength, old_outValue, old_outValueLength );
+
+    return validity;
+}
+
 bool skipPostconditions( bool result,
-                         char * buf,
+                         const char * buf,
                          size_t * start,
                          size_t old_start,
                          size_t max,
@@ -198,7 +222,7 @@ bool skipPostconditions( bool result,
 }
 
 bool skipCollectionPostconditions( JSONStatus_t result,
-                                   char * buf,
+                                   const char * buf,
                                    size_t * start,
                                    size_t old_start,
                                    size_t max )
@@ -209,17 +233,17 @@ bool skipCollectionPostconditions( JSONStatus_t result,
     return validity;
 }
 
-bool skipScalarsPreconditions( char * buf,
+bool skipScalarsPreconditions( const char * buf,
                                size_t * start,
                                size_t max,
                                char mode )
 {
     return ( ( mode == '{' ) || ( mode == '[' ) )
-           & isValidBoundedBufferWithStartIndex( buf, max, start );
+           & isValidBufferWithStartIndex( buf, max, start );
 }
 
 bool skipAnyScalarPostconditions( bool result,
-                                  char * buf,
+                                  const char * buf,
                                   size_t * start,
                                   size_t old_start,
                                   size_t max )
@@ -230,17 +254,17 @@ bool skipAnyScalarPostconditions( bool result,
     return validity;
 }
 
-bool skipDigitsPreconditions( char * buf,
+bool skipDigitsPreconditions( const char * buf,
                               size_t * start,
                               size_t max,
                               int32_t * outValue )
 {
     return ( outValue == NULL || allocated( outValue, sizeof( *outValue ) ) )
-           & isValidBoundedBufferWithStartIndex( buf, max, start );
+           & isValidBufferWithStartIndex( buf, max, start );
 }
 
 bool skipDigitsPostconditions( bool result,
-                               char * buf,
+                               const char * buf,
                                size_t * start,
                                size_t old_start,
                                size_t max,