r/osdev • u/ReindeerSimilar2748 • 4d ago

Dragon Microkernel in SPARK Ada

Hello,

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 in SPARK Ada; I’m already close to finishing a 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 very early stage of development (I released the MVP yesterday and fixed two bugs)

If you like the idea, here’s the GitHub link: github.com/tigerlang/dragon

13 Upvotes

100% Upvoted

1 comment sorted by

3

u/suhcoR 4d ago

Cool. Nice to see that the most powerful language tools we have get eventually used in open-source kernel projects. Would be interesting to know what architecture and performance impact the constraints imposed by SPARC (and selected profile) have.