Dear all,
I saw this blog post in the AdaCore blog, which is a great resource, and I think some of you may like it! Formally Verified Hashed Sets in Ada SPARK | AdaCore Also, from what I have seen, Claire is one of the main developers of GNATprove, so we owe her quite a lot 
Best regards,
Fer