I played with very little introductory programs only. SPARK is the formally verifiable subset of ada from what I recall but my suggestion was to use the ada (ad

I played with very little introductory programs only. SPARK is the formally verifiable subset of ada from what I recall but my suggestion was to use the ada (ada95?) supported by gcc which means there is no special setup needed other than configure gcc. Ada kernel modules have be written but I don't know if any were mainlined.