Let $S$ be a noetherian scheme and let $A$ be an abelian scheme on $S$ with dual $A^\vee$. The generalised Barsotti Weil formula states that there is a canonical and functorial (in $S$ and $A$) isomorphism of groups

$$A^\vee(S) \cong \mathrm{Ext}^1_S(A,\mathbb G_m)$$

the classical version being the special case where $S$ is the spectrum of an algebraically closed field. There are at least two references for this in the literture: The standard one is Oort's LNM on commutative group schemes, where he proves that the Barsotti--Weil formula over $S$ holds if it holds over all residue fields of $S$. He then says that the formula is known to hold over any field and quotes Serre's Groupes algébriques et corps de classes, VII.16, théorème 6. The other one is by Milne, exactly along the same lines and also quoting Serre.

My problem with this is that Serre makes right at the beginning of chapter VII in loc. cit. the assumption that the ground field is *algebraically closed*.

Hence, as long as all residue fields of $S$ are perfect Oort's proof is fine (functoriality in $S$, so one can go down with Galois). For the general case one should/must check that Serre's arguments also work over separably closed fieds. A first careless walkthrough didn't reveal any serious problem with that, so probably everything is just fine. Since "probably just fine" is not good enough:

Here is my request: A proof of the Barsotti--Weil formula over separably closed fields, preferably a reference, but I will appreciate any text or note where this is carefully checked.

By the way: Even if one is only interested in abelian varieties over, say, a finite field, it is important to have Barsotti--Weil over all schemes of finite type over that field, the reason is that one often wants to fppf--sheafify the Barsotti--Weil isomorphism so to get an isomorpihsm of abelian varieties $A^\vee \cong \underline{\mathrm{Ext}}^1(A,\mathbb G_m)$ over the ground field.