Kirill Ziborov

Software Engineer with almost 3 years of experience who is comfortable working with interactive theorem provers such as Isabelle/HOL, HOL4, Coq and model checkers. Also blockchain developer, especially interested in the development and formal verification of smart contracts.

Иванников Институт системного программирования РАН @старший научный сотрудник (01.2022 – настоящее время)  @• Участвовал в разработке фреймворка для верификации программ на языке C в Isabelle/HOL; @• Участвовал в разработке методов доказательства с кэшированием и трассировкой для тактики динамических кадров; @• Моделируемые структуры данных и операторы языка Си;   @• Формально верифицированные компоненты ОС с использованием разработанного фреймворка; @• Читал лекции об Изабель/ХОЛ.

LEON GROUP LLC
Software Engineer (05.2022 – Present) 
• Developed smart contracts for TAIF filling station network in HOL4; 
• Contributed to the development of the InnoChain blockchain node;
• Formally verified properties of smart contracts in HOL4.

INNOPOLIS UNIVERSITY
Software Engineer (07.2020 – 04.2022) 
• Developed a formal model of the HotStuff consensus algorithm; 
• Formally verified the HotStuff consensus algorithm using TLC model checker;
• Developed smart contracts for the InnoChain blockchain in HOL4;
• Developed a framework for deductive verification of smart contracts in HOL4;
• Formally verified properties of smart contracts in HOL4.

Combined Bs & Ms, Mathematics
Lomonosov Moscow State University (09/2017 - 06/2023), Moscow, Russia
-Participated in the organization and attended workshops on formal verification;
-Theoretical research in the field of formal verification and cryptographic protocols.