I am looking for a modern proof of the so-called "Theorem of the Base"--that the Neron-Severi rank of a smooth projective variety is finite. One can prove this for varieties over $\mathbb{C}$ easily via transcendental methods---however, the most recent proof I can find which works e.g. in positive characteristic is due to Lang and Neron and is written in the language of Weil's foundations. (Lang includes a similar proof in his book "Diophantine Geometry.")

Does anyone know of a proof written in the language of schemes?

My motivation is that I'd like to have a brief reading seminar on this theorem with some graduate students at my institution---while it looks like the Lang/Neron paper is translatable, I think that this sort of translation is a serious burden for seminar participants. So it would be nice to have a more modern reference.

arithmeticcontent of the Lang/Neron proof, which is also contained here (math.stanford.edu/~conrad/papers/Kktrace.pdf) in rather more detail (BCnrd pointed me to this article via email). I think I can extract the geometric content from Lang, so this probably suffices. $\endgroup$