| Target | Verification Code | Tool |
|---|---|---|
| MCS Lock | model_check_mcslock.rs | loom |
| RW Lock | model_check_rwlock.rs | loom |
| Cooperative Async/await Scheduler | cooperative | TLA+ |
| Exception Handler of AArch64 | exception.S | TLA+ |
| Context Switch of AArch64 | context/aarch64 | TLA+ |
| Context Switch of x86_64 | context/x86 | TLA+ |
| Delta List | unit test | Kani |
| Ring Queue | unit test | Kani |
| Sleep CPU (no_std) | awkernel_async_lib/src/task/wake_workers_no_std | SPIN |
| Sleep CPU (std) | awkernel_async_lib/src/task/wake_workers | SPIN |
| if_net | awkernel_lib/src/net/if_net | SPIN |
| PrioritizedFIFOScheduler | awkernel_async_lib/src/task/preemptive_spin | SPIN |
| barrier.rs | awkernel_async_lib/src/barrier | TLA+ |