# RustHorn: CHC-based Verification for Rust Programs (full version)

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Feb 2020.

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

- [VeriSafe Agent: Safeguarding Mobile GUI Agent via Logic-based Action Verification](https://mlsanity.com/paper/2503.18492/) (2025)
- [Token Budgets: An Empirical Catalog of 63 LLM-Agent Budget-Overrun Incidents, with an Affine-Typed Rust Mitigation as a Case Study](https://mlsanity.com/paper/2606.04056/) (2026)
- [Chronosymbolic Learning: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning](https://mlsanity.com/paper/2305.01206/) (2023)
- [Verification Modulo Tested Library Contracts](https://mlsanity.com/paper/2604.15533/) (2026)
- [Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code](https://mlsanity.com/paper/2607.13921/) (2026)

## Abstract (arXiv)

Reduction to the satisfiability problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and memories by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.