← All repos

karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code

GitHub
c-languagecryptographyf-starproofsverification
Browse cluster: Lean4 Formal Verification & Cryptography →
4,607commits
66contributors
12languages

Tech stack & purpose

KaRaMeL is a tool that extracts F* programs to readable C code, enabling verified low-level programs written in F* to be compiled to C while preserving semantics. The project targets programs that verify against a low-level memory model, are first-order, and obey certain restrictions such as non-recursive data types. Built in OCaml, KaRaMeL includes a runtime support library (krmllib) with F* models of C concepts and trusted hand-written C implementations, along with support for multiple build variants and platforms including a WebAssembly backend. The tool is a key component of Project Everest and has been used to implement cryptographic libraries and the TLS 1.3 record layer, with its compilation approach formalized in academic papers relating Low* semantics to CompCert's Clight.

Community & reference links

Languages

OCaml
62.7%
F*
23.5%
C
6.4%
Makefile
4.2%
JavaScript
1.6%
C++
0.9%
Python
0.3%
Nix
0.1%
Shell
0.1%
Batchfile
0.1%
Rust
0.0%
Dune
0.0%

Contributors (top 30 of 66)