seL4 Developers: I apologize in advance if this is not the correct place for this email. I am experimenting with Autocorres as an intern at Rockwell Collin's Advanced Technology Center in Minnesota. My latest experiment is in building a small verified library for manipulation and analysis of adjacency lists. My initial work towards this end generated the following error: exception CTERM raised (line 948 of "~/development/rockwellcollins/verification/l4v/tools/autocorres/utils.ML"): autocorres: Internal var uu_::"int" is exposed. Please notify the AutoCorres maintainers of this failure. In the meantime, use "autocorres [keep_going]" to ignore the failure. I am using the latest version of Autocorres and Isabelle. The c and theory file that generated this error can be found here: https://github.com/chaosape/autocorresexperiments/tree/master/graph Thanks! Dan DaCosta