One of recent works of Armando Solar-Lezama that’s advising our new contributor, @jkoppel. He mainly does research in program synthesis. This one overlaps between that and verification of data structures I’ve been submitting. The most interesting other one I’ve seen on data structures is still Imperative/HOL given they were going from functional specs to imperative implementations around C++‘s speed in a popular logic. Like COGENT, that’s helpful since it might cut verification time by an order of magnitude in projects where one can use it.