The ST monad, originally devised by Launchbury and Peyton Jones, allows Haskell programmers to write imperative code (with mutable variables, arrays, etc.) while obtaining a pure interface to that code.
More concretely, the polymorphic type of the entry point function
runST :: (forall s. ST s a) -> a
ensures that all side-effects of the ST computation is contained, and the resulting value is pure.
Has this ever been rigorously (or even formally) proven?
It just so happens that Amin Timany et al. have published a paper at POPL2018 about exactly this topic, titled
Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal:
A Logical Relation for Monadic Encapsulation of State
Proving contextual equivalences in the presence of runST
https://dl.acm.org/doi/10.1145/3158152
Four years later, there is another paper on this, now proving that adding ST preserves all equational properties of the language (in a simply typed call-by-value language):
Koen Jacobs, Dominique Devriese, Amin Timany:
Purity of an ST monad: full abstraction by semantically typed back-translation