If you are willing to adopt a strong enough type system pretty much any interesting property about a program you want to prove is provable. Its just a matter of ergonomics, more complex type systems provide power, but require investment in understanding, both conceptually, and in modeling your problem.

You can also adopt automated verification techniques that can prove strong properties about a system automatically.