# Embracing a mechanized formalization gap

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Oct 2019.

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

- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)

## Abstract (arXiv)

If a code base is so big and complicated that complete mechanical verification is intractable, can we still apply and benefit from verification methods? We show that by allowing a deliberate mechanized formalization gap we can shrink and simplify the model until it is manageable, while still retaining a meaningful, declaratively documented connection to the original, unmodified source code. Concretely, we translate core parts of the Haskell compiler GHC into Coq, using hs-to-coq, and verify invariants related to the use of term variables.