TLA+ [1] and Idris come to mind.
Also Clojure Spec [2]
For the specific case you mention, "taint analysis" would be appropriate.
[1] https://softwareengineeringdaily.com/2018/11/09/tla-with-les... [2] https://www.youtube.com/watch?v=oyLBGkS5ICk Edit: links