My papers Sapir, Mark V.; Birget, Jean-Camille; Rips, Eliyahu Isoperimetric and isodiametric functions of groups. Ann. of Math. (2) 156 (2002), no. 2, 345--466. arXiv:9811105
Birget, J.-C.; Olʹshanskii, A. Yu.; Rips, E.; Sapir, M. V. Isoperimetric functions of groups and computational complexity of the word problem. Ann. of Math. (2) 156 (2002), no. 2, 467--518. arXiv:9811106
disprove the Harvey Friedman's grand conjecture because arbitrary recursive functions are considered there.
Update: I am no longer sure that these papers are "counterexamples". It looks like I misunderstood the question. At least the theorems there are about finite objects (Turing machines and group presentations, computable numbers). But the proofs do not produce large functions. Of course some of the groups that can be constructed by the procedures described in the papers will have solvable word problem (which is also a finitary problem) in the ordinary sense but unsolvable word problem in the sense of EFA. But this is not explicitly written in the papers (because I and other co-authors did not know what EFA is till today).
