Could program verification techniques prevent bugs of the genre of Heartbleed from occurring?
To answer your question in the most concise way - yes, this bug could have potentially been caught by formal verification tools. Indeed, the property "never send a block which is bigger than the size of the hearbeat that was sent" is fairly simple to formalize in most specification languages (e.g. LTL). 

The problem (which is a common criticism against formal methods) is that the specifications you use are written by humans. Indeed, formal methods only shift the bug-hunting challenge from finding the bugs to defining what bugs are. This is a difficult task.

Also, formally verifying software is notoriously difficult due to the state-explosion problem. In this case, it is especially relevant, since many times in order to avoid the state explosion, we abstract away bounds. For example, when we want to say "every request is followed by a grant, within 100000 steps", we need a very long formula, so we abstract it to the formula "every request is eventually followed by a grant". 

Thus, in the heartbleed case, even while attempting to formalize the requirements, the bound in question could have been abstracted away, resulting in the same behavior.

To sum up, potentially this bug could have been avoided by using formal methods, but there would have had to be a human specifying this property in advance.