|
|
|
|
|
|
by markusde
87 days ago
|
|
|
In addition to Cedar: [1] SymCrypt (MSR). Verified cryptographic primitives. It's in the latter style, using the Aeneas model of Rust. [2] KLR (AWS). ML compiler. Not verified, but it's in the former style where they use pure Lean functions and interface with C code across the FFI. [3] SampCert (AWS). Verified random sampling algorithms for differential privacy. Uses pure Lean functions and is called into via the reverse FFI. Full disclosure I worked on 2 and 3 haha. There's also some stuff being used by cryptocurrency people but I don't follow that very closely. [1] https://www.microsoft.com/en-us/research/blog/rewriting-symc...
[2] https://github.com/leanprover/KLR
[3] https://github.com/leanprover/SampCert |
|
|