Using static code analysis, Polyspace Client for Ada and Polyspace Server for Ada provide code verification that proves the absence of overflow, divide-by-zero, out-of-bounds array access, and certain other run-time errors in source code.
Release Notes
https://www.mathworks.com/help/polyspace_ada/release-notes.html