Ada / SPARK can do that. Ada has had some form of that analyses since the first version from 1983.

https://learn.adacore.com/courses/intro-to-spark/chapters/03...