Formal verification has become increasingly important because of the kinds of guarantees that it can provide for software systems. Verification of models of biological and medical systems is a promising application of formal verification. Human neural networks have recently been emulated and studied as a biological system. In this paper, we provide a model of some crucial neuronal circuits, called "archetypes", in the Coq Proof Assistant and prove properties concerning their dynamic behavior. Understanding the behavior of these modules is crucial because they constitute the elementary building blocks of bigger neuronal circuits. We consider seven fundamental archetypes (simple series, series with multiple outputs, parallel composition, positive loop, negative loop, inhibition of a behavior, and contralateral inhibition), and prove an important representative property for six of them. In building up to our model of archetypes, we also provide a general model of "neuronal circuits", and prove a variety of general properties about neurons and circuits. In addition, we have defined our model with a longer term goal of modelling the composition of basic archetypes into larger networks, and structured our libraries with definitions and lemmas useful for proving the properties in this paper as well as those to be proved as future work.

翻译：形式化验证因其能为软件系统提供保证而日益重要。生物与医学系统模型的验证是形式化验证的一个有前景的应用方向。人类神经网络作为生物系统，近年来已被模拟和研究。本文在Coq证明助手中构建了若干关键神经回路（称为“原型”）的模型，并证明了其动态行为的性质。理解这些模块的行为至关重要，因为它们是构成更大神经回路的基本构建单元。我们考虑了七种基本原型（简单串联、多输出串联、并联结构、正反馈环、负反馈环、行为抑制以及对侧抑制），并对其中的六种原型证明了重要的代表性质。在构建原型模型的过程中，我们还提出了“神经回路”的通用模型，并证明了关于神经元和回路的多种通用性质。此外，我们的模型设计着眼于将基本原型组合成更大网络的长期目标，通过定义和引理构建的库结构，不仅服务于本文性质的证明，也为后续研究奠定基础。