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.
If I remember correctly, there is a safe dialect of Ada but it was difficult to setup on Linux. Is that still the case ?