diff --git a/verification/verifast/proof/nathan/README.md b/verification/verifast/proof/nathan/README.md
deleted file mode 100644
index d8b83cacb..000000000
--- a/verification/verifast/proof/nathan/README.md
+++ /dev/null
@@ -1,3 +0,0 @@
-This directory contains proof artifacts written by Nathan Chong.
-See the following pull request:
-https://github.com/FreeRTOS/FreeRTOS/pull/836
diff --git a/verification/verifast/proof/single_core_proofs/README.md b/verification/verifast/proof/single_core_proofs/README.md
new file mode 100644
index 000000000..b74905862
--- /dev/null
+++ b/verification/verifast/proof/single_core_proofs/README.md
@@ -0,0 +1,3 @@
+This directory contains proof artifacts written by Aalok Thakkar and Nathan Chong.
+See the following pull request:
+https://github.com/FreeRTOS/FreeRTOS/pull/836
diff --git a/verification/verifast/proof/nathan/list_predicates.h b/verification/verifast/proof/single_core_proofs/list_predicates.h
similarity index 100%
rename from verification/verifast/proof/nathan/list_predicates.h
rename to verification/verifast/proof/single_core_proofs/list_predicates.h
diff --git a/verification/verifast/proof/task_predicates.h b/verification/verifast/proof/task_predicates.h
index df199649c..02fc7c806 100644
--- a/verification/verifast/proof/task_predicates.h
+++ b/verification/verifast/proof/task_predicates.h
@@ -2,7 +2,7 @@
 
 #define TASKS_GH
 
-#include "nathan/list_predicates.h"
+#include "single_core_proofs/list_predicates.h"
 
 
 /*@