We present our ongoing work on the veriFIRE project: a collaboration between industry and academia, aimed at applying verification to increase the reliability of a real-world, safety-critical system. Specifically, we target an airborne platform for wildfire detection, which incorporates two deep neural networks. We present an end-to-end methodology for verifying \textit{consistency properties} in this system. Our approach encodes application-grounded requirements into solver-compatible queries for existing neural network verifiers. We study properties of interest over critical operational scenarios: (i) monotonicity of detector confidence as target intensity increases; and (ii) bounded detector response under physically plausible blur over the sensor. We instantiate these encodings using state-of-the-art neural network verification backends and evaluate them at scale on real background samples. For the first property, all verification queries are solved in under five minutes. For the second property, verification is substantially harder, highlighting key scalability challenges for richer, higher-dimensional specifications. Overall, the results demonstrate that meaningful, domain-specific guarantees can be obtained for industrial systems.

翻译：我们介绍了veriFIRE项目的当前工作——一项工业界与学术界的合作，旨在应用验证技术提升现实世界安全关键系统的可靠性。具体而言，我们针对一个集成两个深度神经网络的机载野火检测平台，提出了一种端到端的一致性属性验证方法。该方法将基于应用场景的需求编码为兼容现有神经网络验证器的求解查询。我们在关键运行场景下研究了两种重要属性：（i）探测器置信度随目标强度递增的单调性；以及（ii）传感器受到物理合理模糊影响时探测器的有界响应。我们采用最先进的神经网络验证后端实例化这些编码，并在真实背景样本上进行了规模化评估。对于第一个属性，所有验证查询均在五分钟内完成求解。对于第二个属性，验证难度显著增加，这凸显了更丰富、更高维规范所面临的可扩展性挑战。总体结果表明，工业系统能够获得具有实际意义的领域特定保证。