To provide evidence that a recursive algorithm actually works maybe?

This is pretty common in the Blockchain space to verify transactions behave correctly when arriving out of sync with tools like Agda, Coq, etc... I assume it's the same on databases & I heard Leslie Lamport give a talk at work where he mentioned AWS used TLA+ to prove some of its properties.