To add on @cusma’s excellent response, when working with fixed-size integer in critical software, you should be doing a **semi-formal or formal range analysis.**

Concretely, for any integer x in your smart contract, you want to show that it is always between values a and b, where a and b can be represented by the integer chosen (i.e., they fit in 64 bits)

To do that semi-formally, you first show that when initializing the smart contract, this is the case. (A trivial example is when the integer is 0 at the beginning and the lower bound a is also 0). Then you analyse **all** possible calls to the smart contract and show the following invariant:

if the integer x was between a and b before the call, then during the call and after the call, the integer x stays between a and b

This ensures that at any point x stays between a and b.

This analysis is complex and time-consuming but I believe it is of the outmost importance in critical software, such as smart contracts.

This kind of analysis is done in plane or rocket embedded software for example (often in a slightly more formal and automated way).

If you are dealing with floating point (which TEAL does not have), the analysis is even more complex, as floating point not only have issues with bounds (max and min values) but also with precision. But this is another story. Here, you would most likely need an expert to deal with a critical software with floating point.