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

TL;DR

Meta-F* is a framework that enhances the F* verifier with tactics and metaprogramming, enabling automation of proof tasks, code generation, and improved proof development efficiency.

Contribution

It introduces Meta-F*, a novel effect system extension for F* that integrates tactics and metaprogramming, facilitating proof automation and verified code generation.

Findings

Substantial proof development improvements

Enhanced efficiency and robustness in verification

Effective code generation with verified metaprograms

Abstract

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.