(~ forall x . A(x)) ==> (exists x . ~A(x))
It is valid classically, invalid intuitionistically, and still invalid intuitionistically if you slap a not-not out front of it. It is an example (unless I made a mistake in pronouncing it unprovable) of the kind of formula I was looking for, one that demonstrates the necessity of the full recursive Goedel-Kolmogorov-Gentzen double-negation translation, but sadly it's first-order. I was hoping a nice little example would exist in the propositional fragment, but I'm finally starting to believe that none exists. I guess that means the type-theoretic consequences of a "classically true" modality are only going to be nontrivial in a system which is already saddled with dependent types. That's kind of a bummer.
---
Okay,
trurl just informed me that the fact that "if classically A, then intuitionistically ~~A" holds for the propositional fragment is known as Glivenko's theorem. I feel comforted to know it has someone's name attached to it after all. 