XRPL developers are using formal mathematical proofs to test whether its upcoming lending protocol can enter states that break accounting or drain pooled funds. The work has already found vault invariant failures, payment assertions and rounding bugs that were later patched. It cannot eliminate the off-chain credit risk of borrowers defaulting. https://cryptoslate.com/xrpl-tries-to-mathematically-prove-its-new-lending-market-cannot-be-drained/