Act currently implements 3 backends natively:
SMT: automated proof of postcondition and inductive invariants against the specCoq: manual proof of arbitrary properties against the specHevm: automated equivalence proof between the spec and an implementation in evm