I am currently actively developing the “Dragon” microkernel. However, what sets it apart from Linux and other kernels is, of course, its microkernel architecture, and secondly, the fact that it is written and verified using SPARK Ada (gnatprove).
But that doesn’t mean kernel services have to be written only in SPARK Ada; I added the C SDK so that anyone can write a service. The only downside is that this service isn’t the most secure compared to a gnatprove-verified kernel, but the microkernel architecture makes up for it.
I think the main reason I'm developing this microkernel is to create a proven kernel that can be used in some way on user machines, not just on high-security systems.
Dragon is currently in a early stage of development.
If you like this idea, I'd ask you to take a look at the source code (if you know it) or at the C SDK. The current version is 0.4 (we're close to releasing version 0.5, which will include bug fixes and C SDK documentation).
tigerlang•42m ago
I am currently actively developing the “Dragon” microkernel. However, what sets it apart from Linux and other kernels is, of course, its microkernel architecture, and secondly, the fact that it is written and verified using SPARK Ada (gnatprove).
But that doesn’t mean kernel services have to be written only in SPARK Ada; I added the C SDK so that anyone can write a service. The only downside is that this service isn’t the most secure compared to a gnatprove-verified kernel, but the microkernel architecture makes up for it.
I think the main reason I'm developing this microkernel is to create a proven kernel that can be used in some way on user machines, not just on high-security systems.
Dragon is currently in a early stage of development.
If you like this idea, I'd ask you to take a look at the source code (if you know it) or at the C SDK. The current version is 0.4 (we're close to releasing version 0.5, which will include bug fixes and C SDK documentation).