Mультимодальная верификация распределенных протоколов на Lean

Описание: В докладе представлен Veil — платформа для автоматической и интерактивной верификации систем переходов (transition systems) со специализацией на построении машинных доказательств о конкурентных и распределённых алгоритмах. Veil реализован поверх ассистента доказательств Lean. Он позволяет описывать систему переходов и её спецификацию на простом императивном языке, тестировать ее, и затем, генерируя условия верификации (verification conditions) в логике первого порядка, автоматически доказывать ее корректность с помощью SMT-решателей.

Если автоматическая верификация не справляется или если описание системы требует утверждений в логике высшего порядка, Veil предоставляет интерактивный режим верификации — благодаря тому, что он встроен в универсальный ассистент доказательств. Производительность автоматической верификации в Veil достаточна для практических задач, при этом платформа поддерживает бесшовное совмещение автоматических и интерактивных доказательств спецификаций систем, выходящих за пределы возможностей существующих автоматических систем проверки корректности.

Дата записи: 21 ноября 2025.

Докладчик: Владимир Гладштейн, аспирант в National Univeristy of Singapore, младший научный сотрудник в Amazon Web Services.

Совместное заседание рабочей группы Андрея Михайловича Миронова по формальной верификации мехмата МГУ и Научного семинара, организованного совместными усилиями МФТИ, Сколтеха и ВШЭ и рассчитанного как на специалистов в области блокчейна, так и интересующихся этим направлением исследователей.

#blockchain #blockchaintechnology #блокчейн #MIPT #МФТИ #HSE #ВШЭ #Сколтех #Skoltech #MSU #МГУ #veil #формальнаяверификация #распределенныесистемы #распределенныеалгоритмы #верификацияпротоколов #lean #интерактивныедоказательства #автоматическаяверификация #smtрешатели #условияверификации #системыпереходов #конкурентныеалгоритмы #моделчекинг #tla+ #византийскаяустойчивость #протоколыконсенсуса #свойствабезопасности #свойстваживучести #индуктивныеинварианты #помощникидоказательств #верификацияпо #математическиедоказательства #формальныеметоды #верификацияпрограмм #formalverification #distributedsystems #distributedalgorithms #protocolverification #lean #interactivetheoremproving #automatedverification #smtsolvers #verificationconditions #transitionsystems #concurrentalgorithms #modelchecking #byzantinefaulttolerance #consensusprotocols #safetyproperties #livenessproperties #inductiveinvariants #proofassistants #softwareverification #mathematicalproofs #formalmethods #programverification

Дополнительные материалы, новости и анонсы публикуются в официальной группе в Telegram https://t.me/+Kb41CAVPiJZhNjhi