33 files changed, 77 insertions, 53 deletions
diff --git a/proofs/Makefile b/proofs/Makefile
new file mode 100644
index 00000000..1efedbc7
--- /dev/null
+++ b/proofs/Makefile
@@ -0,0 +1,13 @@
+COQMAKEFILE ?= Makefile.coq
+
+all: $(COQMAKEFILE)
+	$(MAKE) -f $(COQMAKEFILE)
+
+$(COQMAKEFILE): _CoqProject
+	coq_makefile -f _CoqProject -o $(COQMAKEFILE)
+
+clean: $(COQMAKEFILE)
+	$(MAKE) -f $(COQMAKEFILE) clean
+	rm -f $(COQMAKEFILE) $(COQMAKEFILE).conf
+
+.PHONY: all clean
+\ No newline at end of file
diff --git a/proofs/NeKernel/HeapMgr.v b/proofs/NeKernel/HeapMgr.v
new file mode 100644
index 00000000..2c5bb9ca
--- /dev/null
+++ b/proofs/NeKernel/HeapMgr.v
@@ -0,0 +1,10 @@
+(*
+    NectarDriver: Traits keyword.
+
+    The Traits keyword defines formal semantic rules associated with a specific identifier N.
+
+    Author: Amlal El Mahrouss
+    Formalization: January 2026
+*)
+
+Require Import Logic.Classical_Prop.
diff --git a/proofs/_CoqProject b/proofs/_CoqProject
new file mode 100644
index 00000000..62ede86f
--- /dev/null
+++ b/proofs/_CoqProject
@@ -0,0 +1,4 @@
+-R NectarDriver NectarDriver
+
+NectarDriver/Impl.v
+NectarDriver/Trait.v
+\ No newline at end of file
diff --git a/public/cpp_modules/.keep b/public/cpp_modules/.keep
deleted file mode 100644
index e69de29b..00000000
--- a/public/cpp_modules/.keep
+++ /dev/null
diff --git a/public/frameworks/CoreFoundation.fwrk/CoreFoundation.json b/public/frameworks/CoreFoundation.fwrk/CoreFoundation.json
index fa891511..ca700965 100644
--- a/public/frameworks/CoreFoundation.fwrk/CoreFoundation.json
+++ b/public/frameworks/CoreFoundation.fwrk/CoreFoundation.json
@@ -1,7 +1,7 @@
 {
     "compiler_path": "x86_64-w64-mingw32-g++",
     "compiler_std": "c++20",
-    "headers_path": ["../", "./", "../../../dev", "../../../src/kernel"],
+    "headers_path": ["../", "./", "../../../src", "../../../src/kernel"],
     "sources_path": ["src/*.cc"],
     "output_name": "./dist/libCoreFoundation.fwrk.dylib",
     "compiler_flags": [
@@ -19,4 +19,4 @@
       "__CF_64BIT__"
     ]
   }
-  
-\ No newline at end of file
+  
diff --git a/public/frameworks/CoreFoundation.fwrk/headers/Object.h b/public/frameworks/CoreFoundation.fwrk/headers/Object.h
index 6aa1623e..931cc8f9 100644
--- a/public/frameworks/CoreFoundation.fwrk/headers/Object.h
+++ b/public/frameworks/CoreFoundation.fwrk/headers/Object.h
@@ -1,5 +1,5 @@
 
-// Copyright 2024-2025, Amlal El Mahrouss (amlal@nekernel.org)
+// Copyright 2024-2026, Amlal El Mahrouss (amlal@nekernel.org)
 // Licensed under the Apache License, Version 2.0 (see LICENSE file)
 // Official repository: https://github.com/nekernel-org/nekernel
 
diff --git a/public/frameworks/CoreFoundation.fwrk/headers/Ref.h b/public/frameworks/CoreFoundation.fwrk/headers/Ref.h
index c7d9234c..33d5a6c5 100644
--- a/public/frameworks/CoreFoundation.fwrk/headers/Ref.h
+++ b/public/frameworks/CoreFoundation.fwrk/headers/Ref.h
@@ -74,7 +74,7 @@ class CFNonNullRef final CF_OBJECT {
     return fRef;
   }
 
-  CFNonNullRef& operator=(const CFNonNullRef<T>& ref) = delete;
+  CFNonNullRef& operator=(const CFNonNullRef<T>& ref) = default;
   CFNonNullRef(const CFNonNullRef<T>& ref)            = default;
 
  private:
diff --git a/public/frameworks/DiskImage.fwrk/DiskImage.json b/public/frameworks/DiskImage.fwrk/DiskImage.json
index 7b424b11..ee1985a6 100644
--- a/public/frameworks/DiskImage.fwrk/DiskImage.json
+++ b/public/frameworks/DiskImage.fwrk/DiskImage.json
@@ -1,7 +1,7 @@
 {
     "compiler_path": "x86_64-w64-mingw32-g++",
     "compiler_std": "c++20",
-    "headers_path": ["../", "./", "../../../dev", "../../../src/kernel"],
+    "headers_path": ["../", "./", "../../../src", "../../../src/kernel"],
     "sources_path": ["src/*.cc"],
     "output_name": "./dist/libDiskImage.fwrk.dylib",
     "compiler_flags": [
@@ -18,4 +18,4 @@
       "__NE_AMD64__"
     ]
   }
-  
-\ No newline at end of file
+  
diff --git a/public/frameworks/KernelTest.fwrk/KernelTest.json b/public/frameworks/KernelTest.fwrk/KernelTest.json
index 691fbac5..075ded46 100644
--- a/public/frameworks/KernelTest.fwrk/KernelTest.json
+++ b/public/frameworks/KernelTest.fwrk/KernelTest.json
@@ -1,7 +1,7 @@
 {
     "compiler_path": "x86_64-w64-mingw32-g++",
     "compiler_std": "c++20",
-    "headers_path": ["../", "./", "../../../dev", "../../../src/kernel"],
+    "headers_path": ["../", "./", "../../../src", "../../../src/kernel"],
     "sources_path": ["src/*.cc"],
     "output_name": "./dist/libKernelTest.fwrk.dylib",
     "compiler_flags": [
@@ -18,4 +18,4 @@
       "__NE_AMD64__"
     ]
   }
-  
-\ No newline at end of file
+  
diff --git a/public/frameworks/LaunchHelpers.fwrk/LaunchHelpers.json b/public/frameworks/LaunchHelpers.fwrk/LaunchHelpers.json
index 80b9eda8..e006fed6 100644
--- a/public/frameworks/LaunchHelpers.fwrk/LaunchHelpers.json
+++ b/public/frameworks/LaunchHelpers.fwrk/LaunchHelpers.json
@@ -16,4 +16,4 @@
         "kSampleFWVersionLowest=0x0100",
         "__NE_SDK__"
     ]
-}
-\ No newline at end of file
+}
diff --git a/src/kernel/NeKit/CxxAbi.h b/src/kernel/NeKit/CxxAbi.h
index f8a6e50e..245f8d3b 100644
--- a/src/kernel/NeKit/CxxAbi.h
+++ b/src/kernel/NeKit/CxxAbi.h
@@ -1,4 +1,4 @@
-// Copyright 2024-2025, Amlal El Mahrouss (amlal@nekernel.org)
+// Copyright 2024-2026, Amlal El Mahrouss (amlal@nekernel.org)
 // Licensed under the Apache License, Version 2.0 (see LICENSE file)
 // Official repository: https://github.com/nekernel-org/nekernel
 
diff --git a/src/kernel/NeKit/ErrorOr.h b/src/kernel/NeKit/ErrorOr.h
index 4289a890..c8c26717 100644
--- a/src/kernel/NeKit/ErrorOr.h
+++ b/src/kernel/NeKit/ErrorOr.h
@@ -1,4 +1,4 @@
-// Copyright 2024-2025, Amlal El Mahrouss (amlal@nekernel.org)
+// Copyright 2024-2026, Amlal El Mahrouss (amlal@nekernel.org)
 // Licensed under the Apache License, Version 2.0 (see LICENSE file)
 // Official repository: https://github.com/nekernel-org/nekernel
 
diff --git a/src/kernel/NeKit/InitializerList.h b/src/kernel/NeKit/InitializerList.h
index 48f9ea53..8e00e95d 100644
--- a/src/kernel/NeKit/InitializerList.h
+++ b/src/kernel/NeKit/InitializerList.h
@@ -1,4 +1,4 @@
-// Copyright 2024-2025, Amlal El Mahrouss (amlal@nekernel.org)
+// Copyright 2024-2026, Amlal El Mahrouss (amlal@nekernel.org)
 // Licensed under the Apache License, Version 2.0 (see LICENSE file)
 // Official repository: https://github.com/nekernel-org/nekernel
 
@@ -17,7 +17,7 @@ class InitializerList final {
 
   explicit InitializerList(const Type* list) {
     if constexpr (N > 0) {
-      for (auto i = 0UL; i < N; ++i) {
+      for (auto i{0ull}; i < N; ++i) {
         fList[i] = list[i];
       }
     }
@@ -34,6 +34,7 @@ class InitializerList final {
   constexpr SizeT size() const { return N; }
 
   Type* operator->() { return this->begin(); }
+
   Type* operator*() { return this->begin(); }
 
  private:
diff --git a/src/kernel/src/InitializerList.cpp b/src/kernel/src/InitializerList.cpp
index 9f19aacb..6599bd18 100644
--- a/src/kernel/src/InitializerList.cpp
+++ b/src/kernel/src/InitializerList.cpp
@@ -1,4 +1,4 @@
-// Copyright 2024-2025, Amlal El Mahrouss (amlal@nekernel.org)
+// Copyright 2024-2026, Amlal El Mahrouss (amlal@nekernel.org)
 // Licensed under the Apache License, Version 2.0 (see LICENSE file)
 // Official repository: https://github.com/nekernel-org/nekernel
 
diff --git a/src/libDDK/DriverKit/macros.h b/src/libDDK/DriverKit/Defines.h
index 12f9d634..2817d809 100644
--- a/src/libDDK/DriverKit/macros.h
+++ b/src/libDDK/DriverKit/Defines.h
@@ -1,4 +1,4 @@
-// Copyright 2024-2025, Amlal El Mahrouss (amlal@nekernel.org)
+// Copyright 2024-2026, Amlal El Mahrouss (amlal@nekernel.org)
 // Licensed under the Apache License, Version 2.0 (see LICENSE file)
 // Official repository: https://github.com/nekernel-org/nekernel
 
diff --git a/src/libDDK/DriverKit/dev.h b/src/libDDK/DriverKit/Device.h
index c3c12ca4..6511b452 100644
--- a/src/libDDK/DriverKit/dev.h
+++ b/src/libDDK/DriverKit/Device.h
@@ -1,19 +1,29 @@
-// Copyright 2024-2025, Amlal El Mahrouss (amlal@nekernel.org)
+// Copyright 2024-2026, Amlal El Mahrouss (amlal@nekernel.org)
 // Licensed under the Apache License, Version 2.0 (see LICENSE file)
 // Official repository: https://github.com/nekernel-org/nekernel
 
 #ifndef DRIVERKIT_DEV_H
 #define DRIVERKIT_DEV_H
 
-#include <DriverKit/ddk.h>
+#include <DriverKit/DriverKit.h>
 
 struct _DDK_DEVICE;
 
 #define DDK_DEVICE_NAME_LEN (255)
 
+#define DDK_TYPE_SOCKET (1)
+#define DDK_TYPE_FILE (2)
+#define DDK_TYPE_DEVICE (3)
+
+#define DDK_SUB_TYPE_TCP (1)
+#define DDK_SUB_TYPE_UDP (2)
+#define DDK_SUB_TYPE_BT  (3)
+
 /// @brief Kernel Device driver.
 typedef struct _DDK_DEVICE DDK_FINAL {
   char d_name[DDK_DEVICE_NAME_LEN];     // the device name. Could be /./DEVICE_NAME/
+  int  d_type;
+  int  d_subtype;
   void* (*d_read)(void* arg, int len);  // read from device.
   void (*d_write)(void* arg, int len);
   void (*d_wait)(void);                             // write to device.
diff --git a/src/libDDK/DriverKit/ddk.h b/src/libDDK/DriverKit/DriverKit.h
index 2ff2db9e..29bde0a6 100644
--- a/src/libDDK/DriverKit/ddk.h
+++ b/src/libDDK/DriverKit/DriverKit.h
@@ -1,11 +1,11 @@
-// Copyright 2024-2025, Amlal El Mahrouss (amlal@nekernel.org)
+// Copyright 2024-2026, Amlal El Mahrouss (amlal@nekernel.org)
 // Licensed under the Apache License, Version 2.0 (see LICENSE file)
 // Official repository: https://github.com/nekernel-org/nekernel
 
 #ifndef DRIVERKIT_DDK_H
 #define DRIVERKIT_DDK_H
 
-#include <DriverKit/macros.h>
+#include <DriverKit/Defines.h>
 
 struct DDK_STATUS_STRUCT;
 struct DDK_OBJECT_MANIFEST;
diff --git a/src/libDDK/DriverKit/io.h b/src/libDDK/DriverKit/IO.h
index 28cf3038..060f7f9b 100644
--- a/src/libDDK/DriverKit/io.h
+++ b/src/libDDK/DriverKit/IO.h
@@ -1,11 +1,11 @@
-// Copyright 2024-2025, Amlal El Mahrouss (amlal@nekernel.org)
+// Copyright 2024-2026, Amlal El Mahrouss (amlal@nekernel.org)
 // Licensed under the Apache License, Version 2.0 (see LICENSE file)
 // Official repository: https://github.com/nekernel-org/nekernel
 
 #ifndef DRIVERKIT_IO_H
 #define DRIVERKIT_IO_H
 
-#include <DriverKit/str.h>
+#include <DriverKit/String.h>
 
 /// @brief print character into UART.
 DDK_EXTERN void kputc(const char ch);
diff --git a/src/libDDK/DriverKit/ObjectKit/driver_base.h b/src/libDDK/DriverKit/ObjectKit/Base.h
index f5811fb2..4d2f6072 100644
--- a/src/libDDK/DriverKit/ObjectKit/driver_base.h
+++ b/src/libDDK/DriverKit/ObjectKit/Base.h
@@ -5,7 +5,7 @@
 #ifndef DRIVERKIT_OBJECTKIT_DRIVER_BASE_H
 #define DRIVERKIT_OBJECTKIT_DRIVER_BASE_H
 
-#include <libDDK/DriverKit/macros.h>
+#include <libDDK/DriverKit/Defines.h>
 
 #define DDK_DRIVER_IMPL \
   final:                \
diff --git a/src/libDDK/DriverKit/ObjectKit/checksum.h b/src/libDDK/DriverKit/ObjectKit/Checksum.h
index 92c63603..e925f9ca 100644
--- a/src/libDDK/DriverKit/ObjectKit/checksum.h
+++ b/src/libDDK/DriverKit/ObjectKit/Checksum.h
@@ -5,7 +5,7 @@
 #ifndef DRIVERKIT_CHECKSUM_H
 #define DRIVERKIT_CHECKSUM_H
 
-#include <DriverKit/ObjectKit/driver_base.h>
+#include <DriverKit/ObjectKit/Base.h>
 
 namespace Kernel::DDK {
 
diff --git a/src/libDDK/DriverKit/ObjectKit/ddk.h b/src/libDDK/DriverKit/ObjectKit/DriverKit.h
index 2d6dec75..490e7d03 100644
--- a/src/libDDK/DriverKit/ObjectKit/ddk.h
+++ b/src/libDDK/DriverKit/ObjectKit/DriverKit.h
@@ -5,7 +5,7 @@
 #ifndef DRIVERKIT_DDK_H
 #define DRIVERKIT_DDK_H
 
-#include <DriverKit/ObjectKit/checksum.h>
-#include <DriverKit/ObjectKit/driver_base.h>
+#include <DriverKit/ObjectKit/Checksum.h>
+#include <DriverKit/ObjectKit/Base.h>
 
 #endif
diff --git a/src/libDDK/DriverKit/str.h b/src/libDDK/DriverKit/String.h
index 9c1386ab..5f56f95b 100644
--- a/src/libDDK/DriverKit/str.h
+++ b/src/libDDK/DriverKit/String.h
@@ -1,11 +1,11 @@
-// Copyright 2024-2025, Amlal El Mahrouss (amlal@nekernel.org)
+// Copyright 2024-2026, Amlal El Mahrouss (amlal@nekernel.org)
 // Licensed under the Apache License, Version 2.0 (see LICENSE file)
 // Official repository: https://github.com/nekernel-org/nekernel
 
 #ifndef DRIVERKIT_STR_H
 #define DRIVERKIT_STR_H
 
-#include <DriverKit/ddk.h>
+#include <DriverKit/DriverKit.h>
 
 /// @brief DDK equivalent of POSIX's string.h
 /// @file str.h
diff --git a/src/libDDK/DriverKit/net.h b/src/libDDK/DriverKit/net.h
deleted file mode 100644
index ecffb983..00000000
--- a/src/libDDK/DriverKit/net.h
+++ /dev/null
@@ -1,14 +0,0 @@
-// Copyright 2024-2025, Amlal El Mahrouss (amlal@nekernel.org)
-// Licensed under the Apache License, Version 2.0 (see LICENSE file)
-// Official repository: https://github.com/nekernel-org/nekernel
-
-#ifndef DRIVERKIT_NET_H
-#define DRIVERKIT_NET_H
-
-#include <DriverKit/macros.h>
-
-struct DDK_NET_MANIFEST;
-
-/// @brief IFS hooks to plug into the FileMgr.
-
-#endif
diff --git a/src/libDDK/libDDK.json b/src/libDDK/libDDK.json
index e07766b2..ce68f149 100644
--- a/src/libDDK/libDDK.json
+++ b/src/libDDK/libDDK.json
@@ -2,12 +2,12 @@
   "compiler_path": "x86_64-w64-mingw32-gcc",
   "compiler_std": "c++20",
   "headers_path": ["../", "./"],
-  "sources_path": ["src/*.c", "src/*.cpp", "src/*.S"],
+  "sources_path": ["src/*.cpp", "src/*.S"],
   "output_name": "libDDK.dll",
   "compiler_flags": [
     "-ffreestanding",
     "-shared",
-    "-std=c17",
+    "-std=c++20",
     "-fno-rtti",
     "-fno-exceptions",
     "-Wl,--subsystem=17"
@@ -20,5 +20,5 @@
     "kDDKVersionLowest=0x0100",
     "kDDKVersion=0x0100"
   ],
-  "description": "C/C++ Driver Development Kit for the NeKernel stack."
+  "description": "C/C++ Driver Development Kit for the NeKernel System."
 }
diff --git a/src/libDDK/src/ddk_alloc.c b/src/libDDK/src/Allocator.cpp
index 09f3034f..b8bc6b4c 100644
--- a/src/libDDK/src/ddk_alloc.c
+++ b/src/libDDK/src/Allocator.cpp
@@ -6,7 +6,7 @@
 
 ======================================== */
 
-#include <DriverKit/ddk.h>
+#include <DriverKit/DriverKit.h>
 
 /**
   \brief Allocates a new heap on the Kernel's side.
diff --git a/src/libDDK/src/ddk_abi_cxx.cpp b/src/libDDK/src/CxxABI.cpp
index 6a9584db..9863471d 100644
--- a/src/libDDK/src/ddk_abi_cxx.cpp
+++ b/src/libDDK/src/CxxABI.cpp
@@ -2,7 +2,7 @@
 // Licensed under the Apache License, Version 2.0 (see LICENSE file)
 // Official repository: https://github.com/nekernel-org/nekernel
 
-#include <DriverKit/ddk.h>
+#include <DriverKit/DriverKit.h>
 
 void* operator new(size_t sz) {
   if (!sz) ++sz;
diff --git a/src/libDDK/src/ddk_dev.c b/src/libDDK/src/Device.cpp
index 64ecefb6..a4494263 100644
--- a/src/libDDK/src/ddk_dev.c
+++ b/src/libDDK/src/Device.cpp
@@ -6,8 +6,8 @@
 
 ======================================== */
 
-#include <DriverKit/dev.h>
-#include <DriverKit/str.h>
+#include <DriverKit/Device.h>
+#include <DriverKit/String.h>
 
 /// @brief Open a new binary device from path.
 DDK_EXTERN DDK_DEVICE_PTR kopen_dev(const char* devicePath) {
diff --git a/src/libDDK/src/ddk_driver_base.cpp b/src/libDDK/src/DriverBase.cpp
index 0a1f8a99..29e9a9c4 100644
--- a/src/libDDK/src/ddk_driver_base.cpp
+++ b/src/libDDK/src/DriverBase.cpp
@@ -2,5 +2,5 @@
 // Licensed under the Apache License, Version 2.0 (see LICENSE file)
 // Official repository: https://github.com/nekernel-org/nekernel
 
-#include <DriverKit/ObjectKit/driver_base.h>
+#include <DriverKit/ObjectKit/Base.h>
 
diff --git a/src/libDDK/src/ddk_io.c b/src/libDDK/src/IO.cpp
index 7e851eb3..89bfa583 100644
--- a/src/libDDK/src/ddk_io.c
+++ b/src/libDDK/src/IO.cpp
@@ -8,7 +8,7 @@
 
 ======================================== */
 
-#include <DriverKit/io.h>
+#include <DriverKit/IO.h>
 
 DDK_EXTERN void kputc(const char ch) {
   if (!ch) return;
diff --git a/src/libDDK/src/ddk_kernel_call.c b/src/libDDK/src/KernelCall.cpp
index 32ae3a42..f7197062 100644
--- a/src/libDDK/src/ddk_kernel_call.c
+++ b/src/libDDK/src/KernelCall.cpp
@@ -8,7 +8,7 @@
 
 ======================================== */
 
-#include <DriverKit/ddk.h>
+#include <DriverKit/DriverKit.h>
 #include <stdarg.h>
 
 /// @brief this is an internal call, do not use it.
diff --git a/src/libDDK/src/ddk_kernel_call_dispatch.S b/src/libDDK/src/KernelCallDispatch.S
index a607fe40..a607fe40 100644
--- a/src/libDDK/src/ddk_kernel_call_dispatch.S
+++ b/src/libDDK/src/KernelCallDispatch.S
diff --git a/src/libDDK/src/ddk_str.c b/src/libDDK/src/String.cpp
index 3021f84a..6d838676 100644
--- a/src/libDDK/src/ddk_str.c
+++ b/src/libDDK/src/String.cpp
@@ -6,7 +6,7 @@
 
 ======================================== */
 
-#include <DriverKit/str.h>
+#include <DriverKit/String.h>
 
 DDK_EXTERN size_t kstrlen(const char* in) {
   if (in == nil) return 0;
diff --git a/src/libDDK/src/ddk_ver.c b/src/libDDK/src/Version.cpp
index 3679bdef..f99734d3 100644
--- a/src/libDDK/src/ddk_ver.c
+++ b/src/libDDK/src/Version.cpp
@@ -6,7 +6,7 @@
 
 ======================================== */
 
-#include <DriverKit/ddk.h>
+#include <DriverKit/DriverKit.h>
 
 #ifndef kDDKVersionHighest
 #define kDDKVersionHighest 1