diff --git a/SPEC_TEST.md b/SPEC_TEST.md
index 78afaf43..ab6fbeb6 100644
--- a/SPEC_TEST.md
+++ b/SPEC_TEST.md
@@ -18,3 +18,8 @@
 | [Context Switch of x86_64](./awkernel_lib/src/context/x86_64.rs) | [context/x86](./specification/awkernel_lib/src/context/x86/) | TLA+ |
 | [Delta List](./awkernel_async_lib_verified/src/delta_list.rs) | unit test | Kani |
 | [Ring Queue](./awkernel_async_lib_verified/src/ringq.rs) | unit test | Kani |
+| Sleep CPU (no_std) | [awkernel_async_lib/src/task/wake_workers_no_std](./specification/awkernel_async_lib/src/task/wake_workers_no_std) | SPIN |
+| Sleep CPU (std) | [awkernel_async_lib/src/task/wake_workers](./specification/awkernel_async_lib/src/task/wake_workers) | SPIN |
+| [if_net](./awkernel_lib/src/net/if_net.rs) | [awkernel_lib/src/net/if_net](./specification/awkernel_lib/src/net/if_net) | SPIN |
+| PrioritizedFIFOScheduler | [awkernel_async_lib/src/task/preemptive_spin](./specification/awkernel_async_lib/src/task/preemptive_spin) | SPIN |
+| [barrier.rs](./awkernel_async_lib/src/sync/barrier.rs) | [awkernel_async_lib/src/barrier](./specification/awkernel_async_lib/src/barrier) | TLA+ |