Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms.

We introduce Meta-F\(^{\star }\), a tactics and metaprogramming framework for the F\(^\star \) program verifier. The main novelty of Meta-F\(^\star \) 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\(^\star \) can be used to generate verified code automatically.