← All repos

smtml

An SMT solver frontend for OCaml

GitHubformalsec.github.io/smtml/smtml/
alt-ergobitwuzlacolibri2cvc5ocamlsmtsmt-libsymbolic-executionwebassemblyz3
Browse cluster: Static Analysis & Code Quality →
1,332commits
25contributors
10languages

Tech stack & purpose

Smtml is an SMT solver frontend for OCaml that provides a typed expression API and dispatches to multiple solver backends including Z3, CVC5, Bitwuzla, Alt-Ergo, and Colibri2. The project is built in OCaml using the Dune build system, OCamlformat for code formatting, and OUnit2 for testing, with support for WebAssembly and symbolic execution use cases. Behind the project is Formalsec, as evidenced by repository ownership and copyright headers. The system features a parametric encoding layer that translates typed expressions into solver-specific terms, phantom-type safety for expression construction, and optimizations including formula simplification and result caching.

Community & reference links

Languages

OCaml
88.6%
Python
6.5%
Shell
2.9%
SMT
0.5%
Raku
0.4%
Dune
0.3%
Dockerfile
0.3%
Common Lisp
0.3%
Nix
0.2%
Turing
0.1%

Contributors