For specificity, fix ZFC as our axiom system, and assume it's consistent.
If we can prove some proposition $P$, then we can also prove $\square P$, "P is provable (in ZFC)", with some constant-factor additional work to turn each step of the proof into a demonstration that that step can be carried out in (some encoding of) the axioms.
However, this naive approach to conversion inevitably lengthens the proof in question. Are there easy-to-construct examples where the proof of $\square P$ is much shorter than the proof of $P$? Intuitively, this seems like it ought to be the case, as one frequently encounters situations where one can easily see that whatever the answer to a problem, it straightforwardly exists by computation, and this realization takes far less work than the computation itself.
If so, can the difference in length be made huge, in the sense that the shortest proof of $\square P$ is of length $n$, while the shortest proof of $P$ is on the order of $BB(n)$? (This is as good as could be hoped for, since a proof of $\square P$ must be at least as long as the length $k$ of the statement $P$, and we can make a Turing Machine of size $O(k)$ searching for proofs of $P$.)
Let's write "$\Diamond_n P$" for "there is no proof of $\neg P$ of length $<n$." Just as $\Diamond\top$ is shorthand for "ZFC is consistent," the sentence $\Diamond_n\top$ is shorthand for "There is no contradiction in ZFC of length $<n$."
Each sentence of the form $\Box\Diamond_n\top$ is then almost trivially ZFC-provable. We argue (within ZFC) by cases:
If $\Diamond_n\top$ is false, then ZFC proves everything (being inconsistent) and so in particular proves $\Diamond_n\top$.
If $\Diamond_n\top$ is true, then ZFC can prove $\Diamond_n\top$ by simply checking all possible ZFC-proofs of length $<n$.
(This second bulletpoint relies on the fact that ZFC proves its own $\Sigma^0_1$-completeness - see e.g. here.)
Now we go a bit further. For each $e$ which ZFC proves is an index for a total computable function, each appropriately-formulated sentence $$\theta^e_n\equiv\Diamond_{\varphi_e(n)}\top$$ have "provability proofs" not too dependent on $e$ (it only takes constant overhead to describe $\varphi_e$). Specifically:
But we can now whip up an $e$ which is sufficiently fast-growing that for no $n$ is there a ZFC-proof of $\theta_n^e$ of length $<h(n)$.
If you want a bigger gulf, just replace the $h$ above with a needlessly-bigger function $\hat{h}$; the corresponding $\hat{e}$ for $\hat{h}$ will then have the property that no $\theta^\hat{e}_n$ has a ZFC-proof of length $<\hat{h}(n)$, but still for all but finitely many $n$ the sentence $$\Box\theta^\hat{e}_n$$ has a ZFC-proof of length $<h(n)$. The bigger the gulf between $h$ and $\hat{h}$, the bigger the "eventual slowdown" we see.
Meanwhile, there is a sort of computable bound on the slowdown we can see here. Assuming ZFC is $\Sigma_1$-sound, there is a total computable $j$ such that for every sentence $\varphi$, if $\Box\varphi$ has a proof of length $<n$ then $\varphi$ has a proof of length $<j(n)$. This $j$ is simple to describe: first enumerate each of the finitely many sentences with provability proofs of length $<n$, and now search for actual proofs of each such sentence and record the longest such. The second half of this algorithm works if ZFC is $\Sigma_1$-sound.
So there is in fact a computable bound to the slowdown we can have, as long as ZFC is $\Sigma_1$-sound. Meanwhile, if ZFC is not $\Sigma_1$-sound then there is a sentence $\psi$ such that ZFC proves $\Box \psi$ but ZFC does not prove $\psi$, so the question doesn't even make sense without that hypothesis.