For write once and forget type of code like a website implemented by a contractor or throwaway code in Jupyter notebooks, the formal verification has a negative value indeed. For anything complex under maintenance ability to see that code behaves as expected in the edge cases without running it is invaluable.