diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/Makefile.json b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/Makefile.json
new file mode 100644
index 0000000000..fbbf00d79d
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/Makefile.json
@@ -0,0 +1,24 @@
+{
+  "ENTRY": "ulARPRemoveCacheEntryByMac",
+  "NUMBER_OF_CACHE_ENTRIES":6,
+  "CBMCFLAGS":
+  [
+  ],
+  "OBJS":
+  [
+    "$(ENTRY)_harness.goto",
+    "$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_ARP.goto"
+  ],
+  "INSTFLAGS":
+  [
+  ],
+  "DEF":
+  [
+    "ipconfigUSE_ARP_REMOVE_ENTRY=1",
+    "ipconfigARP_CACHE_ENTRIES={NUMBER_OF_CACHE_ENTRIES}"
+  ],
+  "INC":
+  [
+    "$(FREERTOS)/tools/cbmc/include"
+  ]
+}
diff --git a/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/ulARPRemoveCacheEntryByMac_harness.c b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/ulARPRemoveCacheEntryByMac_harness.c
new file mode 100644
index 0000000000..dc71cb65f4
--- /dev/null
+++ b/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ulARPRemoveCacheEntryByMac/ulARPRemoveCacheEntryByMac_harness.c
@@ -0,0 +1,19 @@
+/* Standard includes. */
+#include <stdint.h>
+#include <stdio.h>
+
+/* FreeRTOS includes. */
+#include "FreeRTOS.h"
+
+/* FreeRTOS+TCP includes. */
+#include "FreeRTOS_IP.h"
+#include "FreeRTOS_ARP.h"
+
+
+void harness() {
+	const MACAddress_t xMACAddress;
+
+	/* The pointer passed to ulARPRemoveCacheEntryByMac cannot be NULL
+	 * (see the API definition). */
+	ulARPRemoveCacheEntryByMac( &xMACAddress );
+}