In my second year internship at the MPRI I worked under the supervision of Ralf Jung and Max Vistrup on the Iris-Lean project. There, I focused mainly on porting the program logic interface, including the weakest precondition definition and most relevant lemmas. I also contributed to the proof mode with some tactics, such as wp_bind, wp_pure and iloeb.