[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.