# Autoformalizing Memory Specifications with Agents

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

## Key facts

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

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

- [DeepSeek-V3.2: Pushing the Frontier of Open Large Language Models](https://mlsanity.com/paper/2512.02556/) (2025)
- [AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2402.00386/) (2024)
- [AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL](https://mlsanity.com/paper/2503.19174/) (2025)
- [An Evaluation Benchmark for Autoformalization in Lean4](https://mlsanity.com/paper/2406.06555/) (2024)
- [AssertCoder: LLM-Based Assertion Generation via Multimodal Specification Extraction](https://mlsanity.com/paper/2507.10338/) (2025)
- [FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols](https://mlsanity.com/paper/2504.17226/) (2025)
- [Shift-Left Techniques in Electronic Design Automation: A Survey](https://mlsanity.com/paper/2509.14551/) (2025)
- [A Framework for Formal Verification of DRAM Controllers](https://mlsanity.com/paper/2209.14021/) (2022)
- [DRAMPyML: A Formal Description of DRAM Protocols with Timed Petri Nets](https://mlsanity.com/paper/2602.10654/) (2026)

## Abstract (arXiv)

The primary goal of Design Verification (DV) is to ensure that a proposed chip design implementation (either in code, or physical form) exactly matches its specification and is free of functional errors in order to avoid costly re-designs. Achieving this often demands extensive manual interpretation, translating the specification document into a formal, testable representation. While AI has made progress in DV, current approaches typically focus on narrow, isolated tasks rather than full end-to-end specification compliance of modern chip designs, failing to capture the complexity of real-world verification. Our method automatically formalizes natural language memory chip specifications, for industry relevant Dynamic Random Access Memory (DRAM) standards, into a formal representation called DRAMPyML that can be used for downstream DV tasks like the generation of SystemVerilog assertions, stimulus, and functional coverage. We also release our benchmarking dataset, DRAMBench, which can be used to evaluate the evolution of model capabilities (and new approaches) at hardware autoformalization.