Getting formal methods into everyday use.
I lead the Formal Methods Group at Kaspersky, where we develop and verify KasperskyOS — a microkernel operating system that is secure by design. Our verification covers both the specifications and the code of its trusted and critical components.
Operating systems are most of what I have worked on: access control models, concurrent algorithms, kernel architecture — the parts where a mistake is too expensive to discover late.
I practise formal methods where they pay off: applied to the right problems, saving time and effort, and producing results people can act on. I use whichever method fits the task rather than the one I know best, and when the tooling gets in the way I build my own — most often around visualization and validation, the work that closes the gap between verification engineers and everyone else.
Email Codeberg GitHub LinkedIn
Experience
Kaspersky
Research Development Team Lead
Led the Formal Methods Group of 5 researchers. Directed the group’s projects that included:
- Verification of architectural proposals for KasperskyOS.
- Formalization of a DSL for access control policies.
- Development of a new open source tooling for TLA+.
- Publishing results of the groups work in scientific journals.
Lead Research Developer
Developed the methods and techniques the group relied on, shaped decisions on specification design, development and validation. Took a more proactive role in projects of other team members. Promoted formal methods within and outside the company:
- Gave lectures and talks inside the company.
- Helped organize verification competition among the students.
Senior Research Developer
Conducted multiple verification projects, including:
- Formalization of ARM and x86 memory models.
- Verification of several lock-free queues.
- Verification of the IPC subsystem.
Institute for System Programming (ISP RAS)
- Specified and verified several OS access control models in Event-B.
- Built the verification tooling for large industrial C programs.
- Developed safety property specifications for the Linux kernel, and automated the detection of changes to the internal kernel API.
- Wrote a national standard on verifying formal access control models.
Publications
Denis Efremov, Ilya Shchepetkov — Rodin Workshop 2026, 5–7
Vasil Dyadov, Alexander Kogtenkov, Ilya Shchepetkov — ABZ 2026
DOI PDF
Denis Efremov, Viktoria V. Kopach, Eugene Kornykhin, Victor V. Kuliamin, Alexander K. Petrenko, Alexey V. Khoroshilov, Ilya Shchepetkov — Programming and Computer Software 49(7), 559–565
DOI PDF
Ilja S. Zakharov, Evgeny Novikov, Ilya Shchepetkov — arXiv preprint
DOI arXiv PDF
Petr N. Devyanin, Alexey V. Khoroshilov, Victor V. Kuliamin, Alexander K. Petrenko, Ilya Shchepetkov — Programming and Computer Software 46(7), 443–453
DOI PDF
Denis Efremov, Ilya Shchepetkov — FM 2019 Workshops
DOI arXiv PDF
Mikhail Mandrykin, Jake O’Shannessy, Jacob Payne, Ilya Shchepetkov — FM 2019 Workshops
DOI arXiv PDF
Petr N. Devyanin, Victor V. Kuliamin, Alexander K. Petrenko, Alexey V. Khoroshilov, Ilya Shchepetkov — Programming and Computer Software 42(4), 198–205
DOI
Petr N. Devyanin, Alexey V. Khoroshilov, Victor V. Kuliamin, Alexander K. Petrenko, Ilya Shchepetkov — Ershov Memorial Conference (PSI) 2015, 107–115
DOI PDF
Talks
Rodin Workshop @ FM 2026 · Tokyo, Japan · May 2026
slides
OpenCERT @ FM 2019 · Porto, Portugal · October 2019
slides
Event-B Day 2018 · Tokyo, Japan · November 2018
slides
Rodin Workshop @ ABZ 2014 · Toulouse, France · June 2014
slides
Projects
Event-B tooling: a Rust parser, static checker, CLI and language server, plus headless proving and packaging for the surrounding ecosystem.
Education
Ivannikov Institute for System Programming (ISP RAS)
Moscow Institute of Physics and Technology (MIPT)
MSc, Applied Mathematics
BSc, Applied Mathematics
Teaching
Higher School of Economics
Moscow State University (MSU)