Настоящая статья посвящена развитию методики формальной проверки правильности сетевого взаимодействия. В качестве языка для решения задач формальной проверки правильности сетевого взаимодействия выбрана логика тайлов, а в качестве языка для формулировки этих свойств временная модальная логика. В статье обосновывается такой выбор, рассматриваются принципы проверки правильности (доказательства) сетевого взаимодействия как проверки правильности взаимодействия агентов в мультиагентной системе. Автоматизацию проверки правильности взаимодействия предлагается осуществлять логическими программами, получаемыми в результате перехода от описания сетевого взаимодействия в логике тайлов и требований правильности взаимодействия на языке модальной логики к программе проверки правильности на языке логического программирования Visual Prolog. Методика формальной проверки правильности сетевого взаимодействия иллюстрируется примером получения описания поведения агентов в логике тайлов, свойства обязательной реакции в модальной логике и логической программой для случая трех взаимодействующих агентов: руководителя и двух исполнителей. Обсуждаются перспективы использования предлагаемой методики для других свойств и приложений.