# Synthesis and Verification of Transformer Programs (Technical Report)

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 23 of its 37 references that are in the map.
- First posted on arXiv 18 Feb 2026.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [What Algorithms can Transformers Learn? A Study in Length Generalization](https://mlsanity.com/paper/2310.16028/) (2023)
- [Thinking Like Transformers](https://mlsanity.com/paper/2106.06981/) (2021)
- [What Formal Languages Can Transformers Express? A Survey](https://mlsanity.com/paper/2311.00208/) (2023)
- [Model Interpretability through the Lens of Computational Complexity](https://mlsanity.com/paper/2010.12265/) (2020)
- [Exposing Attention Glitches with Flip-Flop Language Modeling](https://mlsanity.com/paper/2306.00946/) (2023)
- [Masked Hard-Attention Transformers Recognize Exactly the Star-Free Languages](https://mlsanity.com/paper/2310.13897/) (2023)
- [A Formal Framework for Understanding Length Generalization in Transformers](https://mlsanity.com/paper/2410.02140/) (2024)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [Learning Transformer Programs](https://mlsanity.com/paper/2306.01128/) (2023)
- [Counting Like Transformers: Compiling Temporal Counting Logic Into Softmax Transformers](https://mlsanity.com/paper/2404.04393/) (2024)
- [Logical Languages Accepted by Transformer Encoders with Hard Attention](https://mlsanity.com/paper/2310.03817/) (2023)
- [Foundations of Symbolic Languages for Model Interpretability](https://mlsanity.com/paper/2110.02376/) (2021)
- [Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces](https://mlsanity.com/paper/1904.02931/) (2019)
- [Characterizing the Expressivity of Fixed-Precision Transformer Language Models](https://mlsanity.com/paper/2505.23623/) (2025)
- [Knee-Deep in C-RASP: A Transformer Depth Hierarchy](https://mlsanity.com/paper/2506.16055/) (2025)
- [The Counting Power of Transformers](https://mlsanity.com/paper/2505.11199/) (2025)
- [Softmax Transformers are Turing-Complete](https://mlsanity.com/paper/2511.20038/) (2025)
- [Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning](https://mlsanity.com/paper/2405.18548/) (2024)
- [Length Generalization Bounds for Transformers](https://mlsanity.com/paper/2603.02238/) (2026)
- [Extracting Robust Register Automata from Neural Networks over Data Sequences](https://mlsanity.com/paper/2511.19100/) (2025)

## Abstract (arXiv)

C-RASP is a simple programming language that was recently shown to capture concepts expressible by transformers. In this paper, we develop new algorithmic techniques for automatically verifying C-RASPs. To this end, we establish a connection to the verification of synchronous dataflow programs in Lustre, which enables us to exploit state-of-the-art model checkers utilizing highly optimized SMT-solvers. Our second contribution addresses learning a C-RASP program in the first place. To this end, we provide a new algorithm for learning a C-RASP from examples using local search. We demonstrate efficacy of our implementation for benchmarks of C-RASPs in the literature, in particular in connection to the following applications: (1) transformer program optimization, and (2) constrained learning of transformer programs (based on a partial specification).