diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 4881aa00..abad151c 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -29,7 +29,7 @@ jobs:
         run: |
           make -C build/ coverage
           declare -a EXCLUDE=("\*test\*" "\*CMakeCCompilerId\*" "\*mocks\*" "\*source\*")
-          echo ${EXCLUDE[@]} | xargs lcov --rc lcov_branch_coverage=1 -r build/coverage.info -o build/coverage.info
+          echo ${EXCLUDE[@]} | xargs lcov --rc lcov_branch_coverage=1 --ignore-errors unused -r build/coverage.info -o build/coverage.info
           lcov --rc lcov_branch_coverage=1 --list build/coverage.info
       - name: Check Coverage
         uses: FreeRTOS/CI-CD-Github-Actions/coverage-cop@main
@@ -44,7 +44,7 @@ jobs:
         uses: FreeRTOS/CI-CD-Github-Actions/complexity@main
         with:
           path: ./
-          horrid_threshold: 12
+          horrid_threshold: 14
 
   doxygen:
     runs-on: ubuntu-latest
@@ -66,7 +66,7 @@ jobs:
           path: ./
 
   formatting:
-    runs-on: ubuntu-20.04
+    runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
       - name: Check formatting
diff --git a/loop_invariants.patch b/loop_invariants.patch
index 581f1dfd..88ad7b6d 100644
--- a/loop_invariants.patch
+++ b/loop_invariants.patch
@@ -1,11 +1,11 @@
 diff --git a/source/core_json.c b/source/core_json.c
-index d8694f0..761c44b 100644
+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
@@ -26,7 +26,7 @@ index d8694f0..761c44b 100644
   *
 @@ -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 )
@@ -36,7 +36,7 @@ index d8694f0..761c44b 100644
          {
 @@ -103,6 +121,13 @@ static size_t countHighBits( uint8_t c )
      size_t i = 0;
-
+ 
      while( ( n & 0x80U ) != 0U )
 +    assigns( i, n )
 +    loopInvariant (
@@ -61,9 +61,9 @@ index d8694f0..761c44b 100644
 +        decreases( j )
          {
              i++;
-
-@@ -346,6 +378,12 @@ static bool skipOneHexEscape( const char * buf,
-     if( ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) )
+ 
+@@ -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 )
@@ -74,10 +74,10 @@ index d8694f0..761c44b 100644
 +        decreases( end - i )
          {
              uint8_t n = hexToInt( buf[ i ] );
-
-@@ -523,6 +561,9 @@ static bool skipString( const char * buf,
+ 
+@@ -505,6 +543,9 @@ static bool skipString( const char * buf,
          i++;
-
+ 
          while( i < max )
 +        assigns( i )
 +        loopInvariant( *start + 1U <= i && i <= max )
@@ -85,9 +85,9 @@ index d8694f0..761c44b 100644
          {
              if( buf[ i ] == '"' )
              {
-@@ -581,6 +622,9 @@ static bool strnEq( const char * a,
+@@ -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 )
@@ -95,9 +95,9 @@ index d8694f0..761c44b 100644
      {
          if( a[ i ] != b[ i ] )
          {
-@@ -696,6 +740,9 @@ static bool skipDigits( const char * buf,
+@@ -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 )
@@ -105,9 +105,9 @@ index d8694f0..761c44b 100644
      {
          if( !isdigit_( buf[ i ] ) )
          {
-@@ -945,6 +992,9 @@ static void skipArrayScalars( const char * buf,
+@@ -928,6 +975,9 @@ static bool skipArrayScalars( const char * buf,
      i = *start;
-
+ 
      while( i < max )
 +    assigns( i )
 +    loopInvariant( *start <= i && i <= max )
@@ -115,9 +115,9 @@ index d8694f0..761c44b 100644
      {
          if( skipAnyScalar( buf, &i, max ) != true )
          {
-@@ -991,6 +1041,13 @@ static bool skipObjectScalars( const char * buf,
+@@ -982,6 +1032,13 @@ static bool skipObjectScalars( const char * buf,
      i = *start;
-
+ 
      while( i < max )
 +    assigns( i, *start, comma )
 +    loopInvariant(
@@ -129,11 +129,11 @@ index d8694f0..761c44b 100644
      {
          if( skipString( buf, &i, max ) != true )
          {
-@@ -1118,6 +1175,14 @@ static JSONStatus_t skipCollection( const char * buf,
+@@ -1109,6 +1166,14 @@ static JSONStatus_t skipCollection( const char * buf,
      i = *start;
-
+ 
      while( i < max )
-+    assigns( i, depth, c, __CPROVER_object_whole( stack ), ret )
++    assigns( i, depth, c, ret, __CPROVER_object_whole( stack ) )
 +    loopInvariant(
 +        -1 <= depth && depth <= JSON_MAX_DEPTH
 +        && *start <= i && i <= max
@@ -144,9 +144,17 @@ index d8694f0..761c44b 100644
      {
          c = buf[ i ];
          i++;
-@@ -1407,6 +1472,9 @@ static bool objectSearch( const char * buf,
+@@ -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 )
@@ -154,9 +162,9 @@ index d8694f0..761c44b 100644
          {
              if( nextKeyValuePair( buf, &i, max, &key, &keyLength,
                                    &value, &valueLength ) != true )
-@@ -1474,6 +1542,9 @@ static bool arraySearch( const char * buf,
+@@ -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 )
@@ -164,7 +172,7 @@ index d8694f0..761c44b 100644
          {
              if( nextValue( buf, &i, max, &value, &valueLength ) != true )
              {
-@@ -1539,6 +1610,9 @@ static bool skipQueryPart( const char * buf,
+@@ -1538,6 +1610,9 @@ static bool skipQueryPart( const char * buf,
      while( ( i < max ) &&
             !isSeparator_( buf[ i ] ) &&
             !isSquareOpen_( buf[ i ] ) )
@@ -174,9 +182,9 @@ index d8694f0..761c44b 100644
      {
          i++;
      }
-@@ -1585,6 +1659,17 @@ static JSONStatus_t multiSearch( const char * buf,
+@@ -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(
@@ -191,4 +199,4 @@ index d8694f0..761c44b 100644
 +    decreases( queryLength - i )
      {
          bool found = false;
-
+ 
diff --git a/source/core_json.c b/source/core_json.c
index d8694f0c..a01c3931 100644
--- a/source/core_json.c
+++ b/source/core_json.c
@@ -321,8 +321,6 @@ static uint8_t hexToInt( char c )
  *
  * @return true if a valid escape sequence was present;
  * false otherwise.
- *
- * @note For the sake of security, \u0000 is disallowed.
  */
 static bool skipOneHexEscape( const char * buf,
                               size_t * start,
@@ -333,17 +331,16 @@ static bool skipOneHexEscape( const char * buf,
     size_t i = 0U, end = 0U;
     uint16_t value = 0U;
 
-    coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
-    coreJSON_ASSERT( outValue != NULL );
+    coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) && ( outValue != NULL ) );
 
     i = *start;
 #define HEX_ESCAPE_LENGTH    ( 6U )   /* e.g., \u1234 */
     /* MISRA Ref 14.3.1 [Configuration dependent invariant] */
     /* More details at: https://github.com/FreeRTOS/coreJSON/blob/main/MISRA.md#rule-143 */
     /* coverity[misra_c_2012_rule_14_3_violation] */
-    end = ( i <= ( SIZE_MAX - HEX_ESCAPE_LENGTH ) ) ? ( i + HEX_ESCAPE_LENGTH ) : SIZE_MAX;
+    end = i + HEX_ESCAPE_LENGTH;
 
-    if( ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) )
+    if( ( end > i ) && ( end < max ) && ( buf[ i ] == '\\' ) && ( buf[ i + 1U ] == 'u' ) )
     {
         for( i += 2U; i < end; i++ )
         {
@@ -358,7 +355,7 @@ static bool skipOneHexEscape( const char * buf,
         }
     }
 
-    if( ( i == end ) && ( value > 0U ) )
+    if( i == end )
     {
         ret = true;
         *outValue = value;
@@ -382,8 +379,6 @@ static bool skipOneHexEscape( const char * buf,
  *
  * @return true if a valid escape sequence was present;
  * false otherwise.
- *
- * @note For the sake of security, \u0000 is disallowed.
  */
 #define isHighSurrogate( x )    ( ( ( x ) >= 0xD800U ) && ( ( x ) <= 0xDBFFU ) )
 #define isLowSurrogate( x )     ( ( ( x ) >= 0xDC00U ) && ( ( x ) <= 0xDFFFU ) )
@@ -437,8 +432,6 @@ static bool skipHexEscape( const char * buf,
  *
  * @return true if a valid escape sequence was present;
  * false otherwise.
- *
- * @note For the sake of security, \NUL is disallowed.
  */
 static bool skipEscape( const char * buf,
                         size_t * start,
@@ -457,9 +450,6 @@ static bool skipEscape( const char * buf,
 
         switch( c )
         {
-            case '\0':
-                break;
-
             case 'u':
                 ret = skipHexEscape( buf, &i, max );
                 break;
@@ -477,14 +467,6 @@ static bool skipEscape( const char * buf,
                 break;
 
             default:
-
-                /* a control character: (NUL,SPACE) */
-                if( iscntrl_( c ) )
-                {
-                    i += 2U;
-                    ret = true;
-                }
-
                 break;
         }
     }
@@ -934,11 +916,12 @@ static bool skipSpaceAndComma( const char * buf,
  *
  * @note Stops advance if a value is an object or array.
  */
-static void skipArrayScalars( const char * buf,
+static bool skipArrayScalars( const char * buf,
                               size_t * start,
                               size_t max )
 {
     size_t i = 0U;
+    bool ret = true;
 
     coreJSON_ASSERT( ( buf != NULL ) && ( start != NULL ) && ( max > 0U ) );
 
@@ -953,11 +936,19 @@ static void skipArrayScalars( const char * buf,
 
         if( skipSpaceAndComma( buf, &i, max ) != true )
         {
+            /* After parsing a scalar, we must either have a comma (followed by more content)
+             * or be at a closing bracket. If neither, the array is malformed. */
+            if( ( i >= max ) || !isSquareClose_( buf[ i ] ) )
+            {
+                ret = false;
+            }
+
             break;
         }
     }
 
     *start = i;
+    return ret;
 }
 
 /**
@@ -1071,7 +1062,7 @@ static bool skipScalars( const char * buf,
         {
             if( !isSquareClose_( buf[ i ] ) )
             {
-                skipArrayScalars( buf, start, max );
+                ret = skipArrayScalars( buf, start, max );
             }
         }
         else
@@ -1151,14 +1142,22 @@ static JSONStatus_t skipCollection( const char * buf,
                 {
                     depth--;
 
-                    if( ( skipSpaceAndComma( buf, &i, max ) == true ) &&
-                        isOpenBracket_( stack[ depth ] ) )
+                    if( skipSpaceAndComma( buf, &i, max ) == true )
                     {
                         if( skipScalars( buf, &i, max, stack[ depth ] ) != true )
                         {
                             ret = JSONIllegalDocument;
                         }
                     }
+                    else
+                    {
+                        /* After closing a nested collection, if there is no comma found when calling
+                         * skipSpaceAndComma, then we must be at the end of the parent collection. */
+                        if( ( i < max ) && !isMatchingBracket_( stack[ depth ], buf[ i ] ) )
+                        {
+                            ret = JSONIllegalDocument;
+                        }
+                    }
 
                     break;
                 }
diff --git a/test/cbmc/proofs/JSON_Validate/Makefile b/test/cbmc/proofs/JSON_Validate/Makefile
index 9bbf9bc1..0a361d0e 100644
--- a/test/cbmc/proofs/JSON_Validate/Makefile
+++ b/test/cbmc/proofs/JSON_Validate/Makefile
@@ -12,5 +12,6 @@ USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver cadical
 
 USE_FUNCTION_CONTRACTS += skipAnyScalar
 USE_FUNCTION_CONTRACTS += skipCollection
+USE_FUNCTION_CONTRACTS += skipSpace
 
 include ../Makefile-json.common
diff --git a/test/unit-test/core_json_utest.c b/test/unit-test/core_json_utest.c
index f3c29866..8759dde1 100644
--- a/test/unit-test/core_json_utest.c
+++ b/test/unit-test/core_json_utest.c
@@ -103,7 +103,7 @@
     "\"foo\":\"abc\",\"" FIRST_QUERY_KEY "\":" FIRST_QUERY_KEY_ANSWER "}"
 #define JSON_DOC_VARIED_SCALARS_LENGTH                     ( sizeof( JSON_DOC_VARIED_SCALARS ) - 1 )
 
-#define MULTIPLE_VALID_ESCAPES                             "\\\\ \\\" \\/ \\b \\f \\n \\r \\t \\\x12"
+#define MULTIPLE_VALID_ESCAPES                             "\\\\ \\\" \\/ \\b \\f \\n \\r \\t \\u0001"
 #define MULTIPLE_VALID_ESCAPES_LENGTH                      ( sizeof( MULTIPLE_VALID_ESCAPES ) - 1 )
 
 #define JSON_DOC_QUERY_KEY_NOT_FOUND                       "{\"hello\": \"world\"}"
@@ -354,12 +354,6 @@
     "\":{\"" SECOND_QUERY_KEY "\" : \"\\uD83D\\uD83D\"}}"
 #define UNICODE_BOTH_SURROGATES_HIGH_LENGTH                 ( sizeof( UNICODE_BOTH_SURROGATES_HIGH ) - 1 )
 
-/* For security, \u0000 is disallowed. */
-#define UNICODE_ESCAPE_SEQUENCE_ZERO_CP   \
-    "{\"foo\":\"abc\",\"" FIRST_QUERY_KEY \
-    "\":{\"" SECOND_QUERY_KEY "\" : \"\\u0000\"}}"
-#define UNICODE_ESCAPE_SEQUENCE_ZERO_CP_LENGTH    ( sizeof( UNICODE_ESCAPE_SEQUENCE_ZERO_CP ) - 1 )
-
 /* /NUL escape is disallowed. */
 #define NUL_ESCAPE                        \
     "{\"foo\":\"abc\",\"" FIRST_QUERY_KEY \
@@ -580,6 +574,7 @@ void test_JSON_Validate_Legal_Documents( void )
 
     jsonStatus = JSON_Validate( JSON_DOC_MULTIPLE_VALID_ESCAPES,
                                 JSON_DOC_MULTIPLE_VALID_ESCAPES_LENGTH );
+
     TEST_ASSERT_EQUAL( JSONSuccess, jsonStatus );
 
     jsonStatus = JSON_Validate( JSON_DOC_LEGAL_UTF8_BYTE_SEQUENCES,
@@ -802,10 +797,6 @@ void test_JSON_Validate_Illegal_Documents( void )
                                 UNICODE_BOTH_SURROGATES_HIGH_LENGTH );
     TEST_ASSERT_EQUAL( JSONIllegalDocument, jsonStatus );
 
-    jsonStatus = JSON_Validate( UNICODE_ESCAPE_SEQUENCE_ZERO_CP,
-                                UNICODE_ESCAPE_SEQUENCE_ZERO_CP_LENGTH );
-    TEST_ASSERT_EQUAL( JSONIllegalDocument, jsonStatus );
-
     jsonStatus = JSON_Validate( UNICODE_VALID_HIGH_INVALID_LOW_SURROGATE,
                                 UNICODE_VALID_HIGH_INVALID_LOW_SURROGATE_LENGTH );
     TEST_ASSERT_EQUAL( JSONIllegalDocument, jsonStatus );
@@ -1506,14 +1497,6 @@ void test_JSON_Search_Illegal_Documents( void )
                               &outValueLength );
     TEST_ASSERT_EQUAL( JSONNotFound, jsonStatus );
 
-    jsonStatus = JSON_Search( UNICODE_ESCAPE_SEQUENCE_ZERO_CP,
-                              UNICODE_ESCAPE_SEQUENCE_ZERO_CP_LENGTH,
-                              COMPLETE_QUERY_KEY,
-                              COMPLETE_QUERY_KEY_LENGTH,
-                              &outValue,
-                              &outValueLength );
-    TEST_ASSERT_EQUAL( JSONNotFound, jsonStatus );
-
     jsonStatus = JSON_Search( UNICODE_VALID_HIGH_INVALID_LOW_SURROGATE,
                               UNICODE_VALID_HIGH_INVALID_LOW_SURROGATE_LENGTH,
                               COMPLETE_QUERY_KEY,
diff --git a/tools/unity/coverage.cmake b/tools/unity/coverage.cmake
index 3cdbd316..8e80bed9 100644
--- a/tools/unity/coverage.cmake
+++ b/tools/unity/coverage.cmake
@@ -6,6 +6,7 @@ execute_process(
             COMMAND lcov --directory ${CMAKE_BINARY_DIR}
                          --base-directory ${CMAKE_BINARY_DIR}
                          --zerocounters
+                         --rc lcov_branch_coverage=1
 
             COMMAND mkdir -p  ${CMAKE_BINARY_DIR}/coverage
         )
@@ -14,6 +15,7 @@ execute_process( COMMAND lcov --directory ${CMAKE_BINARY_DIR}
                          --base-directory ${CMAKE_BINARY_DIR}
                          --initial
                          --capture
+                         --ignore-errors source
                          --rc lcov_branch_coverage=1
                          --rc genhtml_branch_coverage=1
                          --output-file=${CMAKE_BINARY_DIR}/base_coverage.info
@@ -45,6 +47,7 @@ execute_process(COMMAND ruby
 # capture data after running the tests
 execute_process(
             COMMAND lcov --capture
+                         --ignore-errors source
                          --rc lcov_branch_coverage=1
                          --rc genhtml_branch_coverage=1
                          --base-directory ${CMAKE_BINARY_DIR}