formal verification

Verified Textbook Algorithms

https://github.com/Certora/CertoraProver

https://github.com/CertiGraph/CertiGraph

https://fstar-lang.org/

Satisfiability modulo theories

creusot

• Rust -> Coma -> Why3

prusti

• Rust MIR -> Viper IR
• does not catch panic from unwarp None

Why3

• https://toccata.gitlabpages.inria.fr/toccata/gallery/why3.en.html

Spark

Knuckledragger

Deduce

https://github.com/teorth/estimates

Prove-It

HolPy

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

Metamath Zero

• https://digama0.github.io/mm0/thesis.pdf
• Metamath One - writing proofs
• Metamath C - writing verifed programs

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