Easy to Use

Metalift offers a friendly Python API that makes it easy to analyze LLVM sources, define a target language for synthesis, and encode verification conditions.

Powerful Algorithms Built In

Metalift builds on the modern Rosette synthesis engine and the CVC5 theorem prover, making synthesis more efficient and enabling applications in complex domains.

Designed for Flexibility

A variety of APIs make it easy to adapt Metalift for any task. Metalift has been applied in projects ranging from translating imperative Java to Spark, to synthesizing distributed system logic.