Thank you all very much for your inputs! To summarise: I asked about the possibility of adding ACSL annotations to the codebase and the responses ranged from nonplussed on one end of the spectrum to some degree of enthusiasm on the other. It was suggested that libpsql would be a better initial target than the internals. I appreciated the good, brisk discussion and if anyone else has any other ideas please let us all know.
Regards, Colin
