> (Example: working with length-indexed lists in https://github.com/mit-plv/fiat-crypto was a lot more painful for writing cryptographic algorithms than using plain lists and proving length-preservation separately with tactics. Probably because the length is not an inherent part of the algorithm.)

How does this compare with the verified crypto from project Everest that is used in Firefox? (Fstar / related to miTLS)

Are you proving more / more interesting things? Do they also have pain when dealing with richer type level stuff like length indexed lists?