I still maintain SocialCalc with Dan Bricklin, the inventor of spreadsheets, and we have just shipped a version using Lean, Dafny and LemmaScript. It fails faster whenever a bug is introduced rather than waiting for tests to catch it. We rely on invariants and Lean-checked proofs, so the result becomes proof-carrying code. It now fails much faster.