diff --git a/FreeRTOS/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h b/FreeRTOS/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h
deleted file mode 100644
index 8845621573..0000000000
--- a/FreeRTOS/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h
+++ /dev/null
@@ -1,31 +0,0 @@
-/*
- * FreeRTOS V202212.00
- * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved.
- *
- * 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.
- *
- * https://www.FreeRTOS.org
- * https://github.com/FreeRTOS
- *
- */
-
-eFrameProcessingResult_t publicProcessIPPacket( IPPacket_t * const pxIPPacket,
-                                                NetworkBufferDescriptor_t * const pxNetworkBuffer )
-{
-    prvProcessIPPacket( pxIPPacket, pxNetworkBuffer );
-}
diff --git a/FreeRTOS/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h b/FreeRTOS/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h
deleted file mode 100644
index e0f9c7805e..0000000000
--- a/FreeRTOS/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h
+++ /dev/null
@@ -1,46 +0,0 @@
-/*
- * FreeRTOS V202212.00
- * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved.
- *
- * 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.
- *
- * https://www.FreeRTOS.org
- * https://github.com/FreeRTOS
- *
- */
-
-int32_t publicTCPPrepareSend( FreeRTOS_Socket_t * pxSocket,
-                              NetworkBufferDescriptor_t ** ppxNetworkBuffer,
-                              UBaseType_t uxOptionsLength )
-{
-    prvTCPPrepareSend( pxSocket, ppxNetworkBuffer, uxOptionsLength );
-}
-
-BaseType_t publicTCPHandleState( FreeRTOS_Socket_t * pxSocket,
-                                 NetworkBufferDescriptor_t ** ppxNetworkBuffer )
-{
-    prvTCPHandleState( pxSocket, ppxNetworkBuffer );
-}
-
-void publicTCPReturnPacket( FreeRTOS_Socket_t * pxSocket,
-                            NetworkBufferDescriptor_t * pxNetworkBuffer,
-                            uint32_t ulLen,
-                            BaseType_t xReleaseAfterSend )
-{
-    prvTCPReturnPacket( pxSocket, pxNetworkBuffer, ulLen, xReleaseAfterSend );
-}
diff --git a/FreeRTOS/Test/CBMC/include/cbmc.h b/FreeRTOS/Test/CBMC/include/cbmc.h
index 1d898296af..324e8ea520 100644
--- a/FreeRTOS/Test/CBMC/include/cbmc.h
+++ b/FreeRTOS/Test/CBMC/include/cbmc.h
@@ -33,16 +33,6 @@
 #include "task.h"
 #include "semphr.h"
 
-/* FreeRTOS+TCP includes. */
-#include "FreeRTOS_IP.h"
-#include "FreeRTOS_Sockets.h"
-#include "FreeRTOS_IP_Private.h"
-#include "FreeRTOS_UDP_IP.h"
-#include "FreeRTOS_DNS.h"
-#include "FreeRTOS_DHCP.h"
-#include "NetworkBufferManagement.h"
-#include "NetworkInterface.h"
-
 /*
  * CBMC models a pointer as an object id and an offset into that
  * object.  The top bits of a pointer encode the object id and the