If we assume the existence of large cardinals (as in the latest version of the question) then such trees for $\Pi^1_3$ formulas exist. First let's get a local version, meaning a tree for a given $\Pi^1_3$ formula that works for all posets below a certain cardinality. At the end I will mention how to get trees that work for posets of arbitrary cardinality.

Let $S_1$ be a tree on $\omega \times \omega \times \omega \times \omega$ for a given $\Sigma^1_1$ formula.
Let $\kappa$ be a cardinal. Then $S_1$ has a $\mathord{<}\kappa$-absolute complement $T_1$, which is a tree on $\omega \times \omega \times \omega \times \kappa$, namely the tree of attempts to build a real $x \in p[S_1]$ and a rank function on the tree $(S_1)_x$ with values in $\kappa$.

The tree $T_1$ is a tree for the corresponding $\Pi^1_1$ formula, and it works in every generic extension by a poset of size less than $\kappa$.
From $T_1$ we obtain in a natural way a tree $S_2$ on $\omega \times \omega \times \kappa$ for the corresponding $\Sigma^1_2$ formula. (This tree $S_2$ is just the Shoenfield tree, but we need to pay attention to how it was constructed.)
The tree $S_2$ also works in every generic extension by a poset of cardinality less than $\kappa$.

Now assume that $\kappa$ is measurable. Then by Martin's proof of $\Sigma^1_1$ determinacy, the tree $T_1$ is $\kappa$-homogeneous, which implies that the Shoenfield tree $S_2$ is $\kappa$-weakly homogeneous. Then by Martin and Solovay ("A basis theorem for $\Sigma^1_3$ sets of reals") the tree $S_2$ has a $\mathord{<}\kappa$-absolute complement $T_2$. (This tree $T_2$ is a tree on $\omega \times \omega \times \gamma$ for an ordinal $\gamma$ that is a little bit larger than $\kappa$; its exact value is not very important.)

The Martin–Solovay tree $T_2$ is a tree for the corresponding $\Pi^1_2$ formula, and it works in every generic extension by a poset of cardinality less than $\kappa$.
From $T_2$ we obtain in a natural way a tree $S_3$ on $\omega \times \gamma$ for the corresponding $\Sigma^1_3$ formula. The tree $S_3$ also works in every generic extension by a poset of cardinality less than $\kappa$.

Now assume also that there is a Woodin cardinal $\delta < \kappa$.
Then by Martin and Steel ("A proof of projective determinacy") the fact that $T_1$ is $\kappa$-homogeneous, and therefore $\delta^+$-homogeneous, implies that the tree $T_2$ is $\mathord{<}\delta$-homogeneous. So the tree $S_3$ is $\mathord{<}\delta$-weakly homogeneous, and applying the Martin–Solovay construction again we get a tree $T_3$ for the corresponding $\Pi^1_3$ formula that works in every generic extension by a poset of size less than $\delta$, as desired.

If we want trees for $\Pi^1_3$ formulas that work in generic extensions by posets of arbitrary size, we can assume that there is a proper class of Woodin cardinals, but this is overkill in terms of consistency strength. It suffices to assume that $M_1^\sharp(X)$ exists for every set $X$. This $M_1^\sharp(X)$ is a mouse over $X$ with a Woodin cardinal and a partial measure on top.

If you only want to show that the existence of such trees for $\Pi^1_3$ formulas is *consistent*, rather than showing that it holds in $V$, you can weaken the hypothesis further: given a strong cardinal $\kappa$, it follows from a theorem of Woodin that forcing with $\text{Col}(\omega,2^{2^\kappa})$ creates trees for $\Pi^1_3$ formulas that work in all further generic extensions.

Some references for this material are Steel's paper "The derived model theorem" (as Yizheng mentioned,) Larson's book "The Stationary Tower", and Kanomori's book "The Higher Infinite" (Section 32 in particular.)

7more comments