I hadn’t seen EARS before, looks really useful for documenting system requirements. Example from the blog:
When the input A is below 20 [amperes] for more than 10 [milliseconds], the function B shall set the output C to ACTIVE
I also like the idea that gnatprove can provide a “review” equivalent to a human, if not better.