Did you have previous experience with formal verification and/or dependent types?