IMO, a program failing due to a parse error on the input, and a program failing due to a bounds check are functionally the same thing (provided you are using a language with bounds-checked arrays so you don't segfault). You're just moving the bounds checking from the array access path to the input collecting path. I could be misunderstanding you, though.
My referenced program is just proven for input sizes.
If I wanted to do something to validate an entire program subset similarly, I'd make a type with the bounds I needed that gets fed into that algorithm which is proved for those ranges. This isolates the proved code from user input, but the newtype with range ensures those checks are done prior to being fed into the algorithm. You can't "prove" user input, there has to be validation, but you can force that validation prior to entering the proofed code.
