这里是Andrea Vezzosi的Agda formalization，它证明了runST对于一个具有可读/可写引用的单子是安全和全的。它依赖于假设的参数性，即所涉及定义的自由定理的真实性，这是可以预期的，因为参数性正是forall s.技巧起作用的原因。
然而，证明假设我们不能将值放入类型本身依赖于ST s的STRef s中，在Haskell中，我们可以使用这种依赖来获得循环而不需要递归：

loop :: ()
loop = runST $ do
  x <- newSTRef (pure ())
  writeSTRef x $ do
    y <- readSTRef x
    y
  y <- readSTRef x
  y

可能这个版本的ST单子仍然是安全的，只是没有可证明的writeSTRef和readSTRef的总和。

碰巧的是，Amin Timany等人在POPL2018上发表了一篇论文，题目正是这个主题，

一元状态封装的逻辑关系

在runST存在的情况下证明上下文等效性
你可以找到文件here。充分披露：我自己还没有找到时间把它读透彻：）。