# Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms

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

## Key facts

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

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

- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)

## Abstract (arXiv)

We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of tactics and metaprogramming to discharge assertions not solvable by SMT, or to just simplify them into well-behaved SMT fragments. Plus, Meta-F* can be used to generate verified code automatically. Meta-F* is implemented as an F* effect, which, given the powerful effect system of F*, heavily increases code reuse and even enables the lightweight verification of metaprograms. Metaprograms can be either interpreted, or compiled to efficient native code that can be dynamically loaded into the F* type-checker and can interoperate with interpreted code. Evaluation on realistic case studies shows that Meta-F* provides substantial gains in proof development, efficiency, and robustness.