I am interested in pushing the boundaries of what is possible in software verification as inspired by the recent advances, such as the Loom verification framework (https://ilyasergey.net/publications/) within Lean. If you are interested in finding a project that involves exploring applying it to verifying embedded devices or other systems-oriented languages (e.g. Rust) please get in touch and we can discuss depending on your background.