As I understand it, most if not all formal systems can be codified in $\mathsf{ZFC}$, because this theory is sufficiently strong that it allows us to define strings, manipulate them, and talk about the existence of strings satisfying certain properties. (Perhaps the only restriction, but this may be more of a philosophical point, is that it can not codify theories that are "too large" to be modeled by sets.)
What is a weaker (the weakest?) formal system that allows to do the same? That is, that allows to define a notion of strings, of sequences of strings, of deduction, and which can express the existence of objects (so that relations like $\vdash$ can be defined).
It depends on exactly what we mean by "codify," but for one interpretation the answer is: really really really really really really really REALLY weak. Otherwise ... it's still pretty weak.
Specifically (and looking at the language of arithmetic for simplicity), a theory is $\Sigma_1^0$-complete if it proves every true $\Sigma^0_1$ sentence. Roughly speaking, this means that it can verify all specific computations. Note that (for $A$ appropriate) the sentence "$A$ proves $\varphi$" is $\Sigma^0_1$. Moreover, $\Sigma^0_1$-completeness is basically the key requirement for Godel's first incompleteness theorem to kick in. So it's a natural thing to look at.
It turns out that we get $\Sigma^0_1$-completeness - and hence the first incompleteness phenomenon - with very little at all. Specifically, Robinson's arithmetic $\mathsf{R}$ is $\Sigma^0_1$-complete and consists of the following:
Every quantifier-free sentence true in $\mathbb{N}$ (e.g. "$(1+1)+(1+1)=1+(1+(1+1))$").
For each $k\in\mathbb{N}$, the axiom $\forall x[\underline{k}<x\vee\bigvee_{i\le k}x=\underline{i}]$.
We can go even weaker than $\mathsf{R}$, it turns out, although here things get quite technical; see Section $4$ of this paper of Beklemishev if you're interested.
However, this may be rather unsatisfying. For example, $\mathsf{R}$ can't even prove that $<$ is a linear order, or that addition is commutative, or ... etc. Basically, while it can prove all $\Sigma^0_1$ sentences, it can't prove any interesting "general facts." Even somewhat stronger theories fall short in this respect. A natural thing to look at here is Godel's second incompleteness theorem, which relies on a bit more than the first incompleteness theorem. Exactly what GSIT requires is still somewhat open, but certainly extremely weak theories are strong enough for it to apply: e.g. $I\Sigma_1$, which is a tiny fragment of first-order Peano arithmetic, is already overkill.
The literature on GSIT is a bit more technical, and I'm less familiar with it, but I'll try to add a good source later today.