I think people tend to underestimate the amount of pre/post conditions needed to ensure that software is correct, and when those are explicitly mentioned they become much less readable than you would expect.

I disagree; it looks pretty straight forward to me. I mean, the first thing in the file is an iterator over all addresses on a device that were handed out via SLAAC (as opposed to being manually configured). It makes complete sense to me that this would need the IpDeviceAddresses<Ipv6> lock. You can’t iterate over a list that is being changed by someone else, so you have to hold the lock that prevents it while you do. That’s very obvious and not at all what a proof assistant would generate.