TLA+ [1] and Idris come to mind. Also Clojure Spec [2] For the specific case you mention, "taint analysis" would be appropriate. [1] https://softwareengineeri

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-leslie-lamport/ https://softwareengineeringdaily.com/2018/11/09/tla-with-les... [2] https://www.youtube.com/watch?v=oyLBGkS5ICk https://www.youtube.com/watch?v=oyLBGkS5ICk Edit: links