I think the most applicable formal verification work out there is probably the work that’s been put into Simplicity. I think there’s probably not too much work to match chia lisp against coq/lean/isabelle and the like: byte vectors and pairs are pretty basic building blocks. But when you add cryptographic security assumptions (“the odds of coming up with a valid signature without knowing the private key should be less than 2^{128}”) proving things gets pretty hard.