3 ms·
Do you know if there are some resources or examples of this? Especially actual production stuff, not just side projects or proof of concepts?
by wazHFsRy 7mo ago
Do you know if there are some resources or examples of this? Especially actual production stuff, not just side projects or proof of concepts?
- d_christiansen 7mo agoCedar (https://lean-lang.org/use-cases/cedar/ https://lean-lang.org/use-cases/cedar/) at AWS use an executable Lean model of a system as an oracle for differential testing of a Rust implementation. If you can't run Lean in production, then their approach is compelling. The idea is that you start with a Lean specification, create a fully verified implementation with respect to the spec, and then hook it and the production implementation up to a fuzzer or source or random inputs. Then you can explore a lot of the state space fully automatically.
- justboy1987 7mo ago[flagged]
- markusde 7mo agoIn 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-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library/ https://www.microsoft.com/en-us/research/blog/rewriting-symc... [2] https://github.com/leanprover/KLR https://github.com/leanprover/KLR [3] https://github.com/leanprover/SampCert https://github.com/leanprover/SampCert