There are, but they're not too widely used. Cyclone [1] and SPARK [2] are two examples. Of course many others may have been designed in such a way that they a

There are, but they're not too widely used. Cyclone [1] and SPARK [2] are two examples. Of course many others may have been designed in such a way that they are easily analyzable, without that explicitly being a goal. [1] https://en.wikipedia.org/wiki/Cyclone_(programming_language) https://en.wikipedia.org/wiki/Cyclone_(programming_language) [2] https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language)