btw, I do reference an article that is rich in experiences of formal verification: https://dl.acm.org/doi/10.1145/3624728