On the other side, formal languages like Rocq are designed to express software specifications, like "the smart contract can never end up in a situation where the funds are blocked", and verify them on *all* possible inputs.

This process is called formal verification. ✅