[onox]

SPARK2014 is just a tool (gnatprove), which you don't distribute to others (would be rather pointless). Compiling can be done with gnat from your Linux distro, which usually has the Runtime Library Exception.

[eggy]

Is the compiling part "a bit painful" as @tobiasu comments above? Because that is what I am trying to avoid.