Do you have a background or willing to do a deep dive into Lean Theorem Prover? Do you have an interest in low-level hardware or embedded devices programming? Are you interested in device drivers and making devices that are impossible to hack? Please contact Alex as soon as possible for various projects (some with funding) that are available with immediate start. If the initial project goes well, funding is possible for a much larger effort!