The Mordell-Lang (ML) statement or conjecture concerns the qualitative description of the intersection of a subvariety X of a (semi)abelian variety G with a finitely generated subgroup Gamma of G.
It says that the intersection is essentially a translate of a subgroup. In characteristic 0 this ML statement is a generalization of the Mordell conjecture on finiteness of the number of rational points on curves of genus > 1 over number fields, and both the Mordell conjecture and Mordell-Lang conjecture (char. 0) were proved by Faltings (80's, 90's respectively). Suitable formulations of the Mordell-Lang (and Mordell) statement in positive characteristic fail, at least when the data G and X are over a finite field. So Abramovich and Voloch formulated a so-called "function field" version of Mordell-Lang in positive characteristic. This was proved, using model-theoretic methods, by Hrushovski in the mid 90's, but relying crucially on a certain "black box", related to "Zariski geometries". We give another model-theoretic proof in the case of abelian varieties, avoiding the black box.