formal verification
verified compilers, interpreters
ACL2 theorem prover
Jitawa, Milawa
TLA
https://deepspec.org/
https://www.key-project.org/