Fast check proof
In this article, we prove the safety of fast checks to ensure protocol overcollateralization.
Assumptions

Health factor $H_f$ is more than 1

Credit account has debt (loan plus interest) $D$ and $c_1$ units of asset 1. It's liquidity threshold is $LT_1$, price $p_1$.

Liquidation thresholds are calculated for both assets as
where $dP$ is max price drop during liquidation time, $f_L$  liquidation fee (goes to liquidator), $f_p$  liquidation premium (goes to DAO treasury).

User swaps $\Delta c_1$ units of asset 1 to $\Delta c_2$ asset 2 with liquidation threshold $LT_2$ and price $p_2$.

During swap protocol calculates fast check
and allows trade if and only if fast check is successful
 Gearbox is enough overcollateralized if in case of liquidation protocol can ensure repaying debt $D$ and paying liquidation fee $f_LD$.
Problem formalization / Theorem
To ensure Gearbox protocol's overcollateralization after a financial transaction, it is enough to perform fast checks.
Proof
Our theorem can be written as optimization problem:
Let's define
as Credit Account's Total Value after trade. Here $dp$ means possible price drop during swap (or immediately after it).
It is necessary to proof that $V \ge D/(1f_L)$ under conditions of described in Assumptions section. If this equation is true, than gearbox has enough overcollaterization even in case of liquidations happens next.
Let's find minimum for $V$ equation. We can find minimum using linear programming methods:

If $(1f_p)(1dP_2)\frac{LT_1}{LT_2}>1$, then minimum is reached at $\Delta c_1 = 0$. In this case system stays overcollateralized as there is no any trades/actions.

If $(1f_p)(1dP_2)\frac{LT_1}{LT_2}=1$, then $V=c_1p_1$. Taking into account that at start health factor $H_f\ge 1$ we get $V=c_1p_1=DH_f/LT_1\ge D/LT_1 \ge D/(1dP_1f_pf_L) \ge D/(1f_L)$, so system is overcollateralized.

If $(1f_p)(1dP_2)\frac{LT_1}{LT_2}<1$, then $\Delta c_1 = c_1$ and
Let's compare this equation with $D/(1f_L)$:
Which is equal to
As $H_f \ge 1$ and
(as
for any $f_p,\;f_L\in[0,1]$), we get that
So we get that for case 3 inequality $V\ge D/(1f_L)$ is also true.
Then this inequality is true for all cases and system is always overcollateralized.