This is a very good paper! It could use more code examples, though, especially for global annotations, so even a reader not proficient in Ada/SPARK can see the elegance of it.