Formally verifying Advent of Code using Dijkstra's program construction

That's a lot of manual effort to save just a tiny bit of thinking. The first digit is the largest digit among the first N-1 digits. The second digit is the largest digit to the right of the first digit up to and including the Nth digit. That's it.