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.