database normalization and formal verification aren't on the same level of difficulty in terms of implementation, and we all could do the former from the beginning, if we choose to (nobody ever chooses to)