Yoichi Hirai (zkSecurity) - Your guide to formal verification when machines write Lean proofs