If you are willing to relax the restrictions, and you probably should, model checking is probably worth its weight in gold for these scenarios.

You won’t get proofs but you will spell out your logic in a formal language[0] and each run of the checker will exhaustively check your invariants[1].

[0] Useful because often you will learn something you hadn’t considered.

[1] A proof will guarantee your statements hold over quantifiers that are much too large for a model checker to check exhaustively. But, you can say that for a model of size N, property Y is guaranteed to hold. The “small model theorem,” posits that if there is an error in your specification, it is more likely to show up in a small model. You sacrifice the completeness of proofs but this trade-off has been worth it to me.