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

Understand

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.