Short answer: No. At present there are no results in the Langlands program (or comparable long‑standing problems outside logic/topos theory) whose proofs essentially use Caramello’s “toposes as bridges” methodology. Lafforgue’s remark is aspirational: the Langlands correspondence “looks like” a Morita‑type equivalence between two descriptions of the same structure, and so it is tempting to hope it could someday be expressed/understood via classifying toposes. But to date there is no such realization and no Langlands theorem proved via Caramello’s techniques.

A bit more context:

• What Caramello’s program does provide. Caramello developed a systematic way to transport properties and constructions along equivalences of classifying toposes of geometric theories (Morita equivalence in her sense), thereby unifying proofs and giving conceptual bridges between different mathematical presentations. This has produced:

  • topos‑theoretic reproofs/generalizations of classical dualities (Stone/Priestley–type dualities),
  • a topos‑theoretic recasting of Fraïssé’s construction and related model‑theoretic results,
  • a unifying framework for “Galois–type” correspondences.

  Representative papers include:

  • O. Caramello, Fraïssé’s construction from a topos-theoretic perspective (arXiv:0901.2977; JSL 2010).
  • O. Caramello, A topos-theoretic approach to Stone-type dualities (arXiv:0905.0458; various expositions).
  • O. Caramello, Topos-theoretic Galois theories (see her survey and related preprints around 2011–2014).

  These works do give mathematically clean results, but they are either in logic/model theory or present unified proofs of already known theorems; they are not applications to number theory/Langlands.

• What has not happened. There are, to the best of current knowledge, no published papers that:

  • formulate any part of Langlands as a Morita equivalence of geometric theories in Caramello’s sense, or
  • prove new Langlands results (or other longstanding results in number theory, geometry, etc.) by transporting invariants across an equivalence of classifying toposes.

• Why Lafforgue’s comment shouldn’t be read as an existing application. The Langlands correspondence (classical or geometric) is not presently phrased as an equivalence of Grothendieck toposes or classifying toposes of geometric theories. In geometric Langlands one encounters equivalences of derived/∞‑categorical sheaf‑theoretic objects (D‑modules, derived categories on stacks), which lie in a different categorical world from the 1‑topos/classifying‑topos setting central to Caramello’s framework. Lafforgue’s remark is about a suggestive analogy, not an achieved theorem.

If you are looking specifically for a result “outside logic or set theory, stated without mentioning toposes, whose proof essentially uses Caramello’s bridging technique,” there isn’t a widely accepted example yet. The concrete successes so far are mainly:

• new proofs/unifications of known theorems (Stone/Priestley dualities, Galois‑type correspondences),
• general model‑theoretic results (e.g., Fraïssé theory) recast and sometimes extended.

For a balanced entry point, see:

• O. Caramello, Toposes as bridges (book/surveys), which lays out the program and gives worked examples of the method; and
• subsequent literature citing these works, which, as of now, does not include applications to Langlands.

So the sentiment you quote reflects a hope for future conceptual unification rather than a record of existing applications to the Langlands program.