A Hidden Flaw in Safety-Critical Software, Proven Mathematically

Read full text
Authors: Najih Salhab
Cited by: 0

Abstract

A Brief Statement on the Strength of the Scientific Evidence “This risk does not come from implementation. It comes from a formation assumption: allowing entities to function as propositions without an explicit admissibility witness.” “If your framework allows this, testing will never save you.” I invite PhD students and researchers to verify the results of this study for themselves: https://zenodo.org/records/18216160 While empirical sciences rely on experiments and observations—an approach that is powerful but inherently non-certain—this study is based on a constructive mathematical proof that has been mechanically verified. The study does not say we believe or we observed.It demonstrates that: If a system is designed in this way, then this structural vulnerability necessarily exists. This is not a matter of human opinion or probabilistic inference, but a logical fact, mechanically verified using two fully independent tools: Z3 Cubical Agda Agreement between two independent verification systems means that the result is objectively checkable by any researcher and does not rely on authority or trust. A mechanically verified mathematical proof provides a level of logical certainty that empirical experimentation alone cannot offer—just as the fact that2 + 2 = 4does not require a laboratory experiment to be established. Conclusion This evidence does not require a vote or committee approval.All it requires is to run the code and verify it yourself.

Fields of Study & Subjects

Logic programming and type systems Formal Methods in Verification Safety Systems Engineering in Autonomy

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
27 January 2026