Welcome to Formulog!

Formulog is a programming language that extends the logic programming language Datalog with SMT solving and first-order functional programming. Formulog was designed to be a domain-specific language for implementing SMT-based program analyses, like refinement type checking and symbolic execution. But who knows—maybe it will also have other uses!

Questions? Feedback? Please raise a GitHub issue!