[synack]

Out of bounds access would raise a runtime exception, so absence of runtime exceptions proves that cannot happen. Recent versions of SPARK add functionality similar to Rust’s borrow checker as well.

You can find more information in the users guide. https://docs.adacore.com/spark2014-docs/html/ug/index.html