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

International audienceWe 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