Formally verified mixnets in PVS theorem prover. We extract C code from the formalisation, that can be compiler with CompCert to ensure the correctness all the way to assembly level.
mukeshtiwari/Mixnets
Formally verified mixnets in PVS theorem prover. We extract C code from the formalisation, that can be compiler with CompCert to ensure the correctness all the way to assembly level.
Apache-2.0