Formula size lower bounds for AC0 functions
A nice question! Khrapchenko can definitely not give quadratic lower bounds for $AC^0$ functions. His lower bound is in fact at least square of average sensitivity. And all functions in $AC^0$ have poly-logarithmic average sensitivity. Subbotovskaya-Andreev can apparently also not give such a function because the argument they use (random restriction results in much smaller formulas) is exactly the reason forcing large $AC^0$ circuit size; Hastad's Switching Lemma (am not quite sure, just an intuition). The only hope is Nechiporuk. But his argument cannot give more than $n^2/\log n$, by information theoretic reasons. So, can it be that everything in $AC^0$ has formulas of quadratic (or even smaller) size? I don't believe in it, but couldn't quickly find a counterexample.  

Actually, the Allender-Koucky phenomenon arises also in other context - in graph complexity. Say that a circuit of $2n$ variables represents a bipartite $n\times n$ graph $G$ on vertices $V=\{1,\ldots,2n\}$ if for every input vector $a$ with exactly two 1s is, say, positions $i$ and $j$ ($i\leq n$, $j>n$) the circuit accepts $a$ iff vertices $i$ and $j$ are adjacent in $G$. Problem: exhibit an explicit graph $G$ requiring at least $n^{\epsilon}$ gates to be represented by a monotone $\Sigma_3$-circuit. Seems like an innocent question (since most graphs require about $n^{1/2}$ gates. But any such graph would give us a boolean function of $2m=2\log n$ variables requiring non-monotone log-depth circuits of superlinear size (by results of Valiant). Thus, even proving $n^{\epsilon}$ lower bounds for depth-3 circuits may be a challenge.