software verification

aka formal verification

Ivy uses only the decidable fragment of SMT, see http://microsoft.github.io/ivy/decidability.html

https://github.com/hwayne/lets-prove-leftpad

Kani

• bounded model checking
• https://github.com/otter-sec/solana-verify

Bolero

• fuzzing and property testing front-end framework for Rust

Verus: Verifying Rust Programs using Linear Ghost Types

verified compilers, interpreters

ACL2 theorem prover

Jitawa, Milawa

TLA+ https://learntla.com/

https://p-org.github.io/P/

dafny

• Verification of the Incremental Merkle Tree Algorithm with Dafny
• https://github.com/ConsenSys/evm-dafny

https://kframework.org/

https://deepspec.org/

https://www.key-project.org/

• deductive software verification