If you’re a student or young developer, looking to stand out in a crowded job market, I’d recommend picking up a mid-size systems library or application (zlib, sudo, a TLS stack, sqlite, etc.), and re-write it in Lean. There’s going to be enormous demand for formal verification engineers, and right now basically nobody has experience. You could leapfrog into a senior positiob very quickly with a demonstrated “proof of work” in the field