If I have a code base at SPARK Bronze level and for example I have a procedure that just does say a reasonably complex calculation. I could put said procedure into it’s own package and verify it at Silver or an even higher level. As far as I can see you can’t do that with a nested package or single procedure within a package. What Ada SPARK achieves already dumbfounds me so any more complexity might not be desirable, especially when breaking it into packages isn’t much of a problem. However, I thought it might be worth asking the question of how difficult it would be for SPARK to support verifying one procedure at say Silver whilst the rest of the code base is at Bronze?