Melvin's digital garden

software verification

verified compilers, interpreters

ACL2 theorem prover

Jitawa, Milawa

TLA

https://deepspec.org/

Links to this note