The 15k lines of C are generated. The implementations are written in (and formally verified using) F*, and then the C is generated from the F* code using KaRaMeL.
One should be able to trust the proofs of correctness and never look at (or maintain) the generated C directly.
neuroelectron|10 months ago
frumplestlatz|10 months ago
One should be able to trust the proofs of correctness and never look at (or maintain) the generated C directly.
- https://fstar-lang.org
- https://github.com/FStarLang/karamel
- https://github.com/hacl-star/hacl-star