# Neural Model Checking

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 24 of its 102 references that are in the map.
- First posted on arXiv 31 Oct 2024.

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

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Quantization and Training of Neural Networks for Efficient Integer-Arithmetic-Only Inference](https://mlsanity.com/paper/1712.05877/) (2017)
- [VerilogEval: Evaluating Large Language Models for Verilog Code Generation](https://mlsanity.com/paper/2309.07544/) (2023)
- [Reward Machines: Exploiting Reward Function Structure in Reinforcement Learning](https://mlsanity.com/paper/2010.03950/) (2020)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [Graph Neural Networks Meet Neural-Symbolic Computing: A Survey and Perspective](https://mlsanity.com/paper/2003.00330/) (2020)
- [Safe Nonlinear Control Using Robust Neural Lyapunov-Barrier Functions](https://mlsanity.com/paper/2109.06697/) (2021)
- [Learning Safe Multi-Agent Control with Decentralized Neural Barrier Certificates](https://mlsanity.com/paper/2101.05436/) (2021)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [Certified Reinforcement Learning with Logic Guidance](https://mlsanity.com/paper/1902.00778/) (2019)
- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees](https://mlsanity.com/paper/2210.05308/) (2022)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees](https://mlsanity.com/paper/2312.01456/) (2023)
- [Stochastic Omega-Regular Verification and Control with Supermartingales](https://mlsanity.com/paper/2405.17304/) (2024)
- [Unrestricted Termination and Non-Termination Arguments for Bit-Vector Programs](https://mlsanity.com/paper/1410.5089/) (2014)
- [Fuzzing Hardware Like Software](https://mlsanity.com/paper/2102.02308/) (2021)
- [Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems](https://mlsanity.com/paper/2404.01769/) (2024)
- [Bisimulation Learning](https://mlsanity.com/paper/2405.15723/) (2024)
- [Quantitative Verification with Neural Networks](https://mlsanity.com/paper/2301.06136/) (2023)
- [Ranking Templates for Linear Loops](https://mlsanity.com/paper/1401.5338/) (2014)
- [Decision Tree Learning in CEGIS-Based Termination Analysis](https://mlsanity.com/paper/2104.11463/) (2021)
- [Closure Certificates](https://mlsanity.com/paper/2305.17519/) (2023)
- [Everything You Always Wanted to Know About Generalization of Proof Obligations in PDR](https://mlsanity.com/paper/2105.09169/) (2021)

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

- [Formal Verification of Neural Certificates Done Dynamically](https://mlsanity.com/paper/2507.11987/) (2025)
- [RNN Generalization to Omega-Regular Languages](https://mlsanity.com/paper/2509.02491/) (2025)
- [Learning Representations Through Contrastive Neural Model Checking](https://mlsanity.com/paper/2510.01853/) (2025)
- [Logic-Gated Time-Shared Feedforward Networks for Alternating Finite Automata: Exact Simulation and Learnability](https://mlsanity.com/paper/2604.01228/) (2026)
- [Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models](https://mlsanity.com/paper/2605.15131/) (2026)
- [Cycle-Consistent Neural Explanation of Formal Verification Certificates](https://mlsanity.com/paper/2606.24414/) (2026)

## Abstract (arXiv)

We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every execution of a given system satisfies a desired temporal logic specification. Unlike testing, model checking provides formal guarantees. Its application is expected standard in silicon design and the EDA industry has invested decades into the development of performant symbolic model checking algorithms. Our new approach combines machine learning and symbolic reasoning by using neural networks as formal proof certificates for linear temporal logic. We train our neural certificates from randomly generated executions of the system and we then symbolically check their validity using satisfiability solving which, upon the affirmative answer, establishes that the system provably satisfies the specification. We leverage the expressive power of neural networks to represent proof certificates as well as the fact that checking a certificate is much simpler than finding one. As a result, our machine learning procedure for model checking is entirely unsupervised, formally sound, and practically effective. We experimentally demonstrate that our method outperforms the state-of-the-art academic and commercial model checkers on a set of standard hardware designs written in SystemVerilog.