В статье мы описываем подход для формальной проверки параллельных и распределенных программ на C#. Мы используем технологию Microsoft Roslyn для получения синтаксической и семантической информации об интересных конструкциях в реальном коде, чтобы сгенерировать соответствующий код на модельном языке Promela, предназначенном для описания взаимодействующих систем на основе акторов. Затем мы проверяем проблемы параллельного и распределенного кода, используя предопределенные предикаты LTL для модельной программы. Мы можем определять проблемы гонки данных, неправильное использование блокировок, возможные взаимоблокировки в распределенных сервисных взаимодействиях с использованием подхода проверки модели. Описанный метод может быть использован для построения статического анализатора для платформы .NET.