Formally verifying Advent of Code using Dijkstra's program construction (haripm.com)

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.

Wow, this is certainly a new perspective for solving this problem

I was drilled in using the GCL (and variations on it) in Eindhoven TUE and Amsterdam UvA a long time ago, nice to see it here. Not very practical these days but good for brain.