Advances in program verification?
The powerful formalism you are looking for cannot exist, for otherwise we could solve the halting problem. Here is the sketch of an argument why. 

Consider Hoare triples $\{A\} P \{B\}$ for partial correctness. If  we had a (computable) upper bound that related program length to the lengths of correctness proofs, then we could apply it to the  assertion

$$\{\mathsf{True}\} P \{\mathsf{False}\}.$$ 

This assertion is true exactly when $P$ loops. Since we have assumed a (computable) upper bound for proof length, we can find such a proof, were it to exist, in finite time by brute force search, giving an algorithms for deciding the halting problem. Contradiction. The argument can be adapted for other formal methods.

That means, regardless of the specifics, there will always be short programs with long proofs.  One way to find such programs is to look at difficult or open number theoretic questions like Fermat's last theorem or the twin prime conjecture: you can write short programs that diagonialise over the natural numbers, looking for counterexamples. Proving that such programs  do or do not terminate is likely to be highly involved.

All that being said, the last decade has seen an explosion of work on formal verification and a great deal of progress.