# Reasoning Under Threat: Symbolic and Neural Techniques for Cybersecurity Verification

arXiv: https://arxiv.org/abs/2503.22755 · HTML: https://mlsanity.com/paper/2503.22755/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 69 references that are in the map.
- First posted on arXiv 27 Mar 2025.

## Builds on (most cited first, 17 of 17)

- [Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective](https://mlsanity.com/paper/2206.12227/) (2022)
- [The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap](https://mlsanity.com/paper/2412.06512/) (2024)
- [Extracting Optimal Explanations for Ensemble Trees via Logical Reasoning](https://mlsanity.com/paper/2103.02191/) (2021)
- [Completeness for a First-order Abstract Separation Logic](https://mlsanity.com/paper/1608.06729/) (2016)
- [Modular Labelled Sequent Calculi for Abstract Separation Logics](https://mlsanity.com/paper/1710.10805/) (2017)
- [A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation](https://mlsanity.com/paper/2308.03344/) (2023)
- [Towards Large Language Model Aided Program Refinement](https://mlsanity.com/paper/2406.18616/) (2024)
- [A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search](https://mlsanity.com/paper/1302.4783/) (2013)
- [Proof search for propositional abstract separation logics via labelled sequents](https://mlsanity.com/paper/1307.5592/) (2013)
- [A formalisation of the SPARC TSO memory model for multi-core machine code](https://mlsanity.com/paper/1906.11203/) (2019)
- [GRAVITAS: A Model Checking Based Planning and Goal Reasoning Framework for Autonomous Systems](https://mlsanity.com/paper/1910.01380/) (2019)
- [Silas: High Performance, Explainable and Verifiable Machine Learning](https://mlsanity.com/paper/1910.01382/) (2019)
- [An Executable Formal Model of the VHDL in Isabelle/HOL](https://mlsanity.com/paper/2202.04192/) (2022)
- [MUC-driven Feature Importance Measurement and Adversarial Analysis for Random Forest](https://mlsanity.com/paper/2202.12512/) (2022)
- [Geometric Theory for Program Testing](https://mlsanity.com/paper/2206.02083/) (2022)
- [Cross-chain Sharing of Personal Health Records: Heterogeneous and Interoperable Blockchains](https://mlsanity.com/paper/2410.08762/) (2024)
- [Generically Automating Separation Logic by Functors, Homomorphisms and Modules](https://mlsanity.com/paper/2411.06094/) (2024)

## Built on by (most cited first, 1 of 1)

- [Neuro-Symbolic AI for Cybersecurity: State of the Art, Challenges, and Opportunities](https://mlsanity.com/paper/2509.06921/) (2025)

## Abstract (arXiv)

Cybersecurity demands rigorous and scalable techniques to ensure system correctness, robustness, and resilience against evolving threats. Automated reasoning, encompassing formal logic, theorem proving, model checking, and symbolic analysis, provides a foundational framework for verifying security properties across diverse domains such as access control, protocol design, vulnerability detection, and adversarial modeling. This survey presents a comprehensive overview of the role of automated reasoning in cybersecurity, analyzing how logical systems, including temporal, deontic, and epistemic logics are employed to formalize and verify security guarantees. We examine SOTA tools and frameworks, explore integrations with AI for neural-symbolic reasoning, and highlight critical research gaps, particularly in scalability, compositionality, and multi-layered security modeling. The paper concludes with a set of well-grounded future research directions, aiming to foster the development of secure systems through formal, automated, and explainable reasoning techniques.