Tezcheck is a static analysis tool for Michelson smart contracts that takes advantage of Tezla intermediate representation and is inspired by SoftCheck.
git clone https://github.com/joaosreis/tezcheck.git
cd tezcheck
dune build @install
dune install
opam install https://github.com/joaosreis/tezcheck.git
Developed under the FRESCO project (Formal Verification of Smart Contracts), generously funded by Tezos Foundation.