If we consider $ZF$ instead of $ZFC$, then we can say more. There are examples of such results which are obtained by Krivine, using his method of realizability. For example in the paper Realizability algebras II: New models of ZF+DC the following is stated:
Using the proof-program (Curry-Howard) correspondence, we give a new method to obtain models of $ZF$ and relative consistency results in set theory. We show the relative consistency of $ZF + DC$ + there exists a sequence of subsets of $\mathbb{R}$ the cardinals of which are strictly decreasing + other similar properties of $\mathbb{R}$.
As it is stated in the introduction of the paper:
These results seem not to have been previously obtained by forcing.
see also 50 years after forcing, the Curry-Howard correspondence gives new models of ZF