This is not a full answer, but I think it is worth to mention: we can prove the theory CZF + Full separation + ￢Double complement is consistent!

The proof goes as follows: consider the Lubarsky's first model in [1]. Let $\check{0}(\kappa)=\varnothing$ and $\check{1}(\kappa) = \{\check{0}\upharpoonright (\mathrm{On}\setminus\kappa)\}$. They will behave as 0 and 1 of the model. Furthermore, for each ordinal $\kappa$ define
$$\check{1}_\kappa (\lambda ) = \begin{cases}\varnothing & \text{if }\kappa<\lambda\text{ and} \\ \{\check{0}\upharpoonright (\mathrm{On}\setminus\lambda)\} & \text{otherwise.}\end{cases}$$

I will claim that the element $x\in M_0$, defined by $x(\nu)=\{\check{1}\upharpoonright (\mathrm{On}\setminus\nu)\}$ for every ordinal $\nu$, has no double complement. First, it is tedious to check

$$\kappa \vDash \lnot\lnot (\check{1}_\nu \in x) \iff \forall \lambda \ge \kappa \exists \mu\ge\lambda : \mu\models \check{1}_\nu \in x$$
and the later statement holds: take any $\mu>\max(\lambda, \nu)$. Hence if $y\in M_0$ is a double complement of $x$, then it must contain every $\check{1}_\nu$, which is impossible. (In fact, we need to prove any $y\in M_\xi$ for any $\xi$ cannot be a double complement of $x$. However, its proof is not too different from my proof.)

However, my proof (if correct) has some unsatisfactory points. First, it requires the consistency of ZFC. Lubarsky proved that CZF + Full separation is equiconsistent with the second-order arithmetic [2]. I wonder CZF + Full separation + ￢Double complement is equiconsistent with Second order arithmetic. Kripke models seems not adequate to derive such kind of equiconsistency result (unless we form a Kripke model of CZF over CZF.)
Second, it does not settle my original question: what happenes if we assume the axiom of power set?

---

(Added in Jan 24, 2019) I find that V. H. Hayanhan makes a bunch of result on the axiom of double complement over IZF ([example][1]). But most of his article is written in Russian so it is not easily accessible to me.

---

References

(1) Lubarsky, Robert S. "Independence results around constructive ZF." *Annals of Pure and Applied Logic* 132.2-3 (2005): 209-225.

(2) Lubarsky, Robert S. "CZF and Second Order Arithmetic
." *Annals of Pure and Applied Logic* 141.1-2 (2006): 29-34.


  [1]: http://www.mathnet.ru/links/9a6cf27834fe812f38eda4a5e2a6f35d/im7739.pdf