[churnedgodotdev]

Of course. The checks are performed where the values arrive. If a file or network socket provides a number N that is going to be used as an array index, then N must be proved to be within array bounds at compile time before being used as an array index, which means you are forced to catch the bug at compile time and decide how to signal bad values of N.

[Ygg2]

Ok, but you can't check _runtime_ values at _compile_ time. If you have user input/file system/network supply N (where 0<N<100) you still HAVE to check it somewhere. You still have to have a runtime check when interacting with outside world.

[churnedgodotdev]

Of course, that's what I thought I said in my previous comment but I guess I wasn't crystal clear. The formal verification stack basically tells you, "There's no guarantee 0<N<100 holds if you get N from an I/O stream. N can be anything." So it's your job to insert a runtime check for N<=0 or N>=100 and decide how best to handle that, e.g. panic and quit, or clamp N to a valid range if it makes sense, or avoid accessing the array if it makes sense. But the system won't let you use a possibly out of range N as an array subscript so you are forced to code a solution to this special case "at compile time", typically by inserting a runtime check. Though if you are reading data from a trusted ROM you can also use a pragma or special assert to say, "This data can be trusted to have this invariant" and avoid the runtime check.