diff --git a/source/FreeRTOS_IPv6_Sockets.c b/source/FreeRTOS_IPv6_Sockets.c
index 5e5744dce..c61c21a51 100644
--- a/source/FreeRTOS_IPv6_Sockets.c
+++ b/source/FreeRTOS_IPv6_Sockets.c
@@ -305,7 +305,7 @@ static BaseType_t prv_ntop6_write_zeros( char * pcDestination,
         if( ( pxSet->xIndex + pxSet->xZeroLength ) == xShortCount )
         {
             /* Reached the last index, write a second ":". */
-            if( pxSet->uxTargetIndex <= ( uxSize - 1U ) )
+            if( pxSet->uxTargetIndex < ( uxSize - 1U ) )
             {
                 pcDestination[ pxSet->uxTargetIndex ] = ':';
                 pxSet->uxTargetIndex++;
@@ -365,7 +365,7 @@ static BaseType_t prv_ntop6_write_short( char * pcDestination,
     if( xReturn == pdPASS )
     {
         /* If there is enough space to write a short. */
-        if( pxSet->uxTargetIndex <= ( uxSize - uxBytesPerShortValue ) )
+        if( ( pxSet->uxTargetIndex + uxBytesPerShortValue ) < uxSize )
         {
             /* Write hex value of short. at most 4 + 1 bytes. */
             uxLength = uxHexPrintShort( &( pcDestination[ pxSet->uxTargetIndex ] ),
@@ -391,7 +391,11 @@ static BaseType_t prv_ntop6_write_short( char * pcDestination,
  * @param[in] pvSource The binary address, 16 bytes long..
  * @param[out] pcDestination The human-readable ( hexadecimal ) notation of the
  *                            address.
- * @param[in] uxSize The size of pvDestination. A value of 40 is recommended.
+ * @param[in] uxSize The size of pcDestination. MUST be at least
+ *                   ipSIZE_OF_IPv6_ADDR_STRLEN (40) to hold the longest
+ *                   possible IPv6 text form (39 characters) plus its NUL
+ *                   terminator. If uxSize is smaller, the function may return
+ *                   NULL for inputs that produce maximum-length output.
  *
  * @return pdPASS if the translation was successful or else pdFAIL.
  */
diff --git a/test/cbmc/proofs/FreeRTOS_inet_ntop6/FreeRTOS_inet_ntop6_harness.c b/test/cbmc/proofs/FreeRTOS_inet_ntop6/FreeRTOS_inet_ntop6_harness.c
new file mode 100644
index 000000000..e844dabe9
--- /dev/null
+++ b/test/cbmc/proofs/FreeRTOS_inet_ntop6/FreeRTOS_inet_ntop6_harness.c
@@ -0,0 +1,41 @@
+/* Standard includes. */
+#include <stdint.h>
+#include <stdio.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "task.h"
+#include "queue.h"
+#include "semphr.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_IPv6_Sockets.h"
+
+/* CBMC includes. */
+#include "cbmc.h"
+
+/* Bound on the destination buffer size explored by the proof. */
+#ifndef MAX_BUFFER_SIZE
+    #define MAX_BUFFER_SIZE    42U
+#endif
+
+void harness()
+{
+    uint8_t ucSource[ ipSIZE_OF_IPv6_ADDRESS ];
+    socklen_t uxSize;
+    char * pcDestination;
+
+    /* The longest IPv6 text form is 39 characters plus a NUL terminator, so 40
+     * bytes. The bound is a little above that so the proof covers the exact-fit
+     * and has-room cases as well as the short ones. */
+    __CPROVER_assume( uxSize <= MAX_BUFFER_SIZE );
+
+    /* Back pcDestination with exactly uxSize bytes so that any write at an
+     * index greater than or equal to uxSize is reported. */
+    pcDestination = safeMalloc( uxSize );
+    __CPROVER_assume( pcDestination != NULL );
+
+    ( void ) FreeRTOS_inet_ntop6( ucSource, pcDestination, uxSize );
+}
diff --git a/test/cbmc/proofs/FreeRTOS_inet_ntop6/Makefile.json b/test/cbmc/proofs/FreeRTOS_inet_ntop6/Makefile.json
new file mode 100644
index 000000000..9e2663356
--- /dev/null
+++ b/test/cbmc/proofs/FreeRTOS_inet_ntop6/Makefile.json
@@ -0,0 +1,21 @@
+{
+  "ENTRY": "FreeRTOS_inet_ntop6",
+  "CBMCFLAGS":
+  [
+    "--unwind 9",
+    "--nondet-static"
+  ],
+  "OBJS":
+  [
+    "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv6_Sockets.goto"
+  ],
+  "OPT":
+  [
+    "--export-file-local-symbols"
+  ],
+  "DEF":
+  [
+  ]
+}
diff --git a/test/unit-test/FreeRTOS_Sockets_IPv6/FreeRTOS_Sockets_IPv6_utest.c b/test/unit-test/FreeRTOS_Sockets_IPv6/FreeRTOS_Sockets_IPv6_utest.c
index b79531313..c37c57bdf 100644
--- a/test/unit-test/FreeRTOS_Sockets_IPv6/FreeRTOS_Sockets_IPv6_utest.c
+++ b/test/unit-test/FreeRTOS_Sockets_IPv6/FreeRTOS_Sockets_IPv6_utest.c
@@ -869,6 +869,28 @@ void test_FreeRTOS_inet_ntop6_LesserBufferSizeNonZero( void )
     TEST_ASSERT_EQUAL( NULL, pcReturn );
 }
 
+/**
+ * @brief Test that room for the NUL terminator is reserved within uxSize.
+ *
+ * The longest IPv6 text form is 39 characters, so a 39-byte destination cannot
+ * also hold the terminator. The conversion must fail rather than write at
+ * index 39.
+ */
+void test_FreeRTOS_inet_ntop6_MaxAddressExactSize( void )
+{
+    const char * pcReturn;
+    IPv6_Address_t xMaxAddress;
+    char cDestination[ NTOP_CHAR_BUFFER_SIZE ];
+
+    ( void ) memset( xMaxAddress.ucBytes, 0xFF, ipSIZE_OF_IPv6_ADDRESS );
+    ( void ) memset( cDestination, 0xAA, sizeof( cDestination ) );
+
+    pcReturn = FreeRTOS_inet_ntop6( xMaxAddress.ucBytes, cDestination, NTOP_CHAR_BUFFER_LAST_INDEX );
+
+    TEST_ASSERT_EQUAL( NULL, pcReturn );
+    TEST_ASSERT_EQUAL_UINT8( 0xAA, ( uint8_t ) cDestination[ NTOP_CHAR_BUFFER_LAST_INDEX ] );
+}
+
 /**
  * @brief Test for the case when the incoming character is not a colon.
  */