Neat! Do you have some pointers to your work? I would be especially interested in example verifications of lock free data structures and in comparing the proof effort to logics custom built for this purpose.<p>All the constructions I know use at least second order logic and something like Iris is - as far as I know - most elegantly described internal to the topos of trees. If you have found a good way to avoid this complexity then that&#x27;s a significant contribution.