Рефлекс – процесс-ориентированный язык, который обеспечивает простое в сопровождении программное обеспечение для систем управления. Язык был успешно использован в нескольких критически важных с точки зрения безопасности кибер-физических системах, например в управляющем программном обеспечении для печи выращивания монокристаллического кремния. В настоящее время основной целью языкового проекта Reflex является развитие поддержки для автоматизированной разработки программного обеспечения, ориентированного на критически важные с точки зрения безопасности приложения. В данной статье представлена формальная операционная семантика языка Reflex как базис для применения формальных методов для верификации Reflex программ.