Graduated from the Moscow State University at 2012. Since 2010 is working in the Insitute for System Programming of Russian Academy of Sciences.

Have taughed course on deductive verification of imperative programs in 2013-2016, since 2022 is teaching courses on functional programming with dependent types.

Worked in projects for model-based testing of multi-threaded systems (2010-2011), dynamic modelling of aviation electronics (2011-2019), model-based testing of cryptographic protocols using functional languages (2019-2020), property-based testing using dependent types with DepTyCheck (2020-now). Active contributor to the Idris programming language compiler and infrastructure.