Is there any formal proof that they are PRFs?
In these applications (PSI, PAKE), it's usually not necessary to prove standalone PRF security. Sometimes you can get a secure PSI for example from something that is slightly weaker than a PRF (e.g., a PRF for bounded # of queries).
In this case, the constructions are standalone PRFs, and the proof would follow the same logic as the PSI/PAKE security proofs. I can give an idea of the proof for $H(x)^k$ (in prime-order cyclic groups):
Consider a reduction algorithm $R$ that takes as input a triple of group elements $(K,A,B)$ and does the following: $R$ internally runs a PRF adversary and plays the role of the random oracle $H$ and the construction $F(k,x) = H(x)^k$. Whenever $A$ queries $H(x)$, respond with $A^{r_x}$; whenever $A$ queries $F(x)$, respond with $B^{r_x}$. Here $r_x$ is uniform for each distinct $x$.
If $(K=g^k, A=g^a, B=g^{ak})$ then $B^{r_x} = (g^{ak})^{r_x} = ((g^a)^{r_x})^k = H(x)^k$ so the PRF adversary is seeing true outputs of the PRF.
If $B$ is uniform in $(K,A, B)$, then each $B^{r_x}$ is uniform, so the PRF adversary is seeing random outputs from its PRF oracle.
The two cases of $R$'s inputs $(K,A,B)$ are indistinguishable by the DDH assumption, this shows that the PRF construction is secure.
If they are all PRFs in the random oracle model under DDH assumption, what are the differences between the three constructions?
PSI/PAKE applications are interactive protocols. When we need security against malicious adversaries, there must be a simulator that watches what the adversary does and "explains" it (extracting an input to send to the ideal PSI/PAKE functionality on behalf of the adversary). In the random oracle model, the simulator gets to also observe all of the adversary's queries to the random oracle.
So the reason to use something like $H(x,stuff)$ instead of $H(stuff)$ in such a protocol is to help the simulator extract. If $x$ is right there (as an input to the random oracle) then the simulator's job is much easier. This is a standard trick in malicious-secure PSI (in the random oracle model).