diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json
new file mode 100644
index 000000000..233289079
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json
@@ -0,0 +1,31 @@
+{
+  "ENTRY": "vSocketBind",
+  "ALLOW_SEND_WITHOUT_BIND":"1",
+  "ALLOW_ETHERNET_DRIVER_FILTER":"1",
+  "ALLOW_TCP":"1",
+  "CBMCFLAGS":
+  [
+    "--unwind 1"
+  ],
+  "OBJS":
+  [
+    "$(FREERTOS)/Source/list.goto",
+    "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Sockets.goto",
+    "$(ENTRY)_harness.goto"
+  ],
+  "INSTFLAGS":
+  [
+  ],
+  "DEF":
+  [
+    "ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND={ALLOW_SEND_WITHOUT_BIND}",
+    "ipconfigUSE_TCP={ALLOW_TCP}",
+    "ipconfigETHERNET_DRIVER_FILTERS_PACKETS={ALLOW_ETHERNET_DRIVER_FILTER}"
+  ],
+  "INC":
+  [
+    "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/include",
+    "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/proofs/utility"
+  ]
+}
+
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/vSocketBind_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/vSocketBind_harness.c
new file mode 100644
index 000000000..38c079245
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/vSocketBind_harness.c
@@ -0,0 +1,68 @@
+/* Standard includes. */
+#include <stdint.h>
+#include <stdio.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "list.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_Sockets.h"
+
+#include "memory_assignments.c"
+
+uint16_t prvGetPrivatePortNumber( BaseType_t xProtocol );
+
+
+uint16_t prvGetPrivatePortNumber( BaseType_t xProtocol )
+{
+	uint16_t usResult;
+	return usResult;
+}
+
+BaseType_t xIPIsNetworkTaskReady( void )
+{
+	/* Return true saying that the task is ready. */
+	return pdTRUE;
+}
+
+
+/* Random number generator provided by the application. In our case, CBMC provides
+ * an indeterministic value. */
+BaseType_t xApplicationGetRandomNumber( uint32_t *pulNumber )
+{
+	__CPROVER_assert( pulNumber != NULL, "Argument to xApplicationGetRandomNumber cannot be NULL" );
+
+	if( nondet_bool() )
+	{
+		*pulNumber = nondet_uint32_t();
+		return 1;
+	}
+	else
+	{
+		*pulNumber = NULL;
+		return 0;
+	}
+}
+
+void harness()
+{
+	FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
+
+	__CPROVER_assume( pxSocket != NULL );
+	__CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET );
+
+	struct freertos_sockaddr * pxBindAddress = safeMalloc( sizeof( struct freertos_sockaddr ) );
+
+	/* uxAddressLength is not used in this implementation. */
+	size_t uxAddressLength;
+
+	BaseType_t xInternal;
+
+	/* Call to init the socket list. */
+	vNetworkSocketsInit();
+
+	vSocketBind( pxSocket, pxBindAddress, uxAddressLength, xInternal );
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_SOCKET_SEND_WITHOUT_BIND/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_SOCKET_SEND_WITHOUT_BIND/Makefile.json
new file mode 100644
index 000000000..cb8ae2e50
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_SOCKET_SEND_WITHOUT_BIND/Makefile.json
@@ -0,0 +1,28 @@
+{
+  "ENTRY": "vSocketBind",
+  "ALLOW_SEND_WITHOUT_BIND":"1",
+  "CBMCFLAGS":
+  [
+    "--unwind 1"
+  ],
+  "OBJS":
+  [
+    "$(FREERTOS)/Source/list.goto",
+    "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Sockets.goto",
+    "$(ENTRY)_harness.goto"
+  ],
+  "INSTFLAGS":
+  [
+  ],
+  "DEF":
+  [
+    "ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND={ALLOW_SEND_WITHOUT_BIND}",
+    "ipconfigUSE_TCP=1"
+  ],
+  "INC":
+  [
+    "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/include",
+    "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/proofs/utility"
+  ]
+}
+
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c
new file mode 100644
index 000000000..78278e5ad
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c
@@ -0,0 +1,65 @@
+/* Standard includes. */
+#include <stdint.h>
+#include <stdio.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "list.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_Sockets.h"
+
+#include "memory_assignments.c"
+
+uint16_t prvGetPrivatePortNumber( BaseType_t xProtocol )
+{
+	uint16_t usResult;
+	return usResult;
+}
+
+BaseType_t xIPIsNetworkTaskReady( void )
+{
+	/* Return true saying that the task is ready. */
+	return pdTRUE;
+}
+
+
+/* Random number generator provided by the application. In our case, CBMC provides
+ * an indeterministic value. */
+BaseType_t xApplicationGetRandomNumber( uint32_t *pulNumber )
+{
+        __CPROVER_assert( pulNumber != NULL, "Argument to xApplicationGetRandomNumber cannot be NULL" );
+
+        if( nondet_bool() )
+        {
+                *pulNumber = nondet_uint32_t();
+                return 1;
+        }
+        else
+        {
+                *pulNumber = NULL;
+                return 0;
+        }
+}
+
+void harness()
+{
+	FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
+
+	__CPROVER_assume( pxSocket != NULL );
+	__CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET );
+
+	struct freertos_sockaddr * pxBindAddress = safeMalloc( sizeof( struct freertos_sockaddr ) );
+
+	/* uxAddressLength is not used in this implementation. */
+	size_t uxAddressLength;
+
+	BaseType_t xInternal;
+
+	/* Call to init the socket list. */
+	vNetworkSocketsInit();
+
+	vSocketBind( pxSocket, pxBindAddress, uxAddressLength, xInternal );
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/Makefile.json
new file mode 100644
index 000000000..9cfe12e06
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/Makefile.json
@@ -0,0 +1,28 @@
+{
+  "ENTRY": "vSocketBind",
+  "ALLOW_SEND_WITHOUT_BIND":"0",
+  "CBMCFLAGS":
+  [
+    "--unwind 1"
+  ],
+  "OBJS":
+  [
+    "$(FREERTOS)/Source/list.goto",
+    "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Sockets.goto",
+    "$(ENTRY)_harness.goto"
+  ],
+  "INSTFLAGS":
+  [
+  ],
+  "DEF":
+  [
+    "ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND={ALLOW_SEND_WITHOUT_BIND}",
+    "ipconfigUSE_TCP=1"
+  ],
+  "INC":
+  [
+    "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/include",
+    "$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/proofs/utility"
+  ]
+}
+
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c
new file mode 100644
index 000000000..d9c7c9b3a
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c
@@ -0,0 +1,66 @@
+/* Standard includes. */
+#include <stdint.h>
+#include <stdio.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+#include "list.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_IP_Private.h"
+#include "FreeRTOS_Sockets.h"
+
+#include "memory_assignments.c"
+
+uint16_t prvGetPrivatePortNumber( BaseType_t xProtocol )
+{
+	uint16_t usResult;
+	return usResult;
+}
+
+BaseType_t xIPIsNetworkTaskReady( void )
+{
+	/* Return true saying that the task is ready. */
+	return pdTRUE;
+}
+
+
+/* Random number generator provided by the application. In our case, CBMC provides
+ * an indeterministic value. */
+BaseType_t xApplicationGetRandomNumber( uint32_t *pulNumber )
+{
+        __CPROVER_assert( pulNumber != NULL, "Argument to xApplicationGetRandomNumber cannot be NULL" );
+
+        if( nondet_bool() )
+        {
+                *pulNumber = nondet_uint32_t();
+                return 1;
+        }
+        else
+        {
+                *pulNumber = NULL;
+                return 0;
+        }
+}
+
+void harness()
+{
+	FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
+
+	__CPROVER_assume( pxSocket != NULL );
+	__CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET );
+
+	/* malloc instead of safeMalloc since we do not allow socket without binding. */
+	struct freertos_sockaddr * pxBindAddress = malloc( sizeof( struct freertos_sockaddr ) );
+
+	/* uxAddressLength is not used in this implementation. */
+	size_t uxAddressLength;
+
+	BaseType_t xInternal;
+
+	/* Call to init the socket list. */
+	vNetworkSocketsInit();
+
+	vSocketBind( pxSocket, pxBindAddress, uxAddressLength, xInternal );
+}