I agree that trying to produce this sort of spec for the entire project is probably a fool's errand, but I still see the value for critical components of the sy

I agree that trying to produce this sort of spec for the entire project is probably a fool's errand, but I still see the value for critical components of the system. Formally verifying the correctness of balance calculation from a ledger, or that database writes are always persisted to the write ahead log, for example.