KaRaMeL extracts verified F* programs to C, but only inside a narrow subset

The subset is the whole design, not an implementation detail

KaRaMeL is a tool that extracts an F* program to readable C code, and the README summarises the ambition in four words: K&R meets ML.

The conditions that make the extraction possible are stated up front. If the F* program verifies against a low-level memory model that talks about the stack and the heap, if it is first-order, and if it obeys certain restrictions such as non-recursive data types, then KaRaMeL will turn it into C.

That is a narrow door, and the reason is mathematical rather than practical. The extraction is not a pretty-printer for F* source. It is a semantics-preserving translation, and the paper formalisation states that the compilation of such F* programs to C preserves semantics, starting from Low*, a subset of F*, and relating its semantics to CompCert's Clight.

The restrictions fall out of that goal. A stack and heap memory model gives you a precise, machine-checkable account of where data lives, which is what lets the extracted C be reasoned about. First-order code has no higher-order functions to compile, so the C has a fixed calling convention. Non-recursive data types mean the generated code has no need for a recursive descent in the type representation, so the layout can be fixed at extraction time.

None of that makes the tool unsuitable. It makes the tool specific. A program that satisfies all three conditions is a program whose C output you can argue about with a paper, and a program that does not is simply out of scope.

This is the compiler behind HACL* and the TLS 1.3 record layer

The evidence that KaRaMeL works on real code is quantitative, and it is in the README rather than in a benchmark table.

The authors have written 120,000 lines of Low* code, implementing the TLS 1.3 record layer. As such, KaRaMeL is a key component of Project Everest, and the Low* work in the tutorial linked from the README is the same body of code.

The library behind that code is HACL*, the High Assurance Crypto Library, which provides numerous cryptographic primitives written in F*. These primitives enjoy memory safety, functional correctness, and some degree of side-channel resistance, and they extract to C via KaRaMeL.

That last clause is what makes KaRaMeL interesting beyond cryptography. The C that comes out is readable C, in the style of K&R, and it is C that came from a program with a machine-checked proof. A compiler that could only handle one protocol would be a curiosity. A compiler that has been pointed at a hundred thousand lines of cryptographic code and produced a working TLS record layer is a tool.

The project is hosted under the FStarLang organisation, alongside F* itself, which is the clearest signal about where it sits. F* is the verification language, KaRaMeL is the extraction back end for the subset of F* that can be extracted, and the two are developed together by the same community.

The README also points at a tutorial as the best way to learn KaRaMeL, and notes that pull requests and feedback are welcome.

Building it means OCaml, OPAM, GNU make and a working F*

KaRaMeL requires OCaml (>= 4.10.0), OPAM, and a recent version of GNU make. There is a specific note about make: on OSX, this may require installing a recent GNU make via homebrew and invoking gmake instead of make. There is also a note that on OSX, KaRaMeL is happier if you have greadlink installed, which comes from brew install coreutils.

The OCaml dependencies are installed with a single opam command that pulls in ppx_deriving_yojson, zarith, pprint, menhir at 20161115 or newer, sedlex, process, fix, wasm at 2.0.0 or newer, visitors, ctypes-foreign, ctypes and uucp.

That list is worth a second look because it tells you what kind of program this is. menhir and sedlex are parser generators and lexer generators, zarith is arbitrary precision integers, visitors is for AST traversals, uucp is Unicode, and ctypes-foreign is for calling into C.

Then you need F* itself, either as a binary package or built by running make. The fstar.exe executable should be on your PATH, or you may set the variable FSTAR_EXE to its location. To build, just run make from this directory.

The build itself is a plain make from the repository directory, and the Makefile shows why the F* dependency is conditional. The all target depends on local-install, which depends on krmllib, which depends on minimal, and minimal only needs lib/Version.ml and a dune build. The comment on the minimal target says that if you are just trying to do a minimal build, you do not need F*, and the FSTAR_OCAMLENV variable is assigned lazily so it does not warn if fstar.exe is not there.

So the tool has a two-stage build. You can compile the extractor without F* installed, and F* is only needed for the library build and for the tests that actually extract code. The minimal target, which is the one that does not need F* installed, looks like this:

minimal: lib/Version.ml
	dune build
	ln -sf _build/default/src/Karamel.exe krml

The Makefile encodes a F* version boundary you have to know about

Two details in the Makefile determine whether your build works, and both are about which F* you have.

The first is the FSTAR_EXE variable. The Makefile sets FSTAR_EXE ?= fstar.exe, so it picks up fstar.exe from your PATH by default and you can override it to point at a specific build. The pre target is where the F* environment matters: it evaluates FSTAR_OCAMLENV, which is FSTAR_EXE --ocamlenv, and then checks whether ocamlfind can query fstar.lib. The error message it prints is a direct question, Didn't find fstar.lib via ocamlfind; is F* properly installed?

The second is a version split that the Makefile is explicit about. There is a test-pulse target with the comment that this depends on minimal since fstar2 (with Pulse) is not expected to be able to build krmllib. The default test target goes through all, and therefore through the full krmllib build.

That distinction matters if you are working with the newer F* line. The minimal target is described as creating a top-level ./krml symlink to the built Karamel executable, but it does not build krmllib nor set it up in a way that allows karamel to find its runtime, misc and include directories, so it is somewhat barebones. The local-install target is the full local install, and out/ will contain essentially the same directory as an OPAM install or binary package.

The three directory variables are how the tool finds its own resources. KRML_LIBDIR, KRML_INCLUDEDIR and KRML_MISCDIR are set to the krmllib, include and misc directories in the source tree, which is exactly the set of top-level directories in the repository. So a build from source has the layout of an installed package, and the krmllib build is run with KRML_EXE pointing at the freshly built krml.

The lib/Version.ml target is generated from the git hash, with a fallback to the GIT_REV environment variable, so a build from a tarball without git still gets a version.

Installing through OPAM, and pinning the dev version of both

KaRaMeL is also available on OPAM, by running opam install karamel. The interesting case is the development version, and the README gives the two-step recipe for it.

If you installed the latest version of F* through OPAM, using opam pin add fstar --dev-repo, you can also install the most up-to-date version of KaRaMeL by running opam pin add karamel --dev-repo.

The two commands are a matched pair, and the order matters. The F* pin points the OPAM switch at the F* development repository rather than a released version, and the karamel pin then points at KaRaMeL's development repository. The reason to do this is stated in the tutorial context: KaRaMeL tracks the F* development branch closely enough that a released KaRaMeL may not match a development F*, and vice versa.

This is worth understanding as a policy rather than a trick. KaRaMeL is a component of the F* toolchain, so the F* version determines the frontend, the memory model and the standard library that the extracted code depends on. A mismatch is not a small bug, it can change what the extracted C means.

The documentation is thin on this point in the README itself, which ends the build section with the instruction to run make test if you have the right version of F* and fstar.exe in your PATH. The right version is left to the reader, which is a real gap for anyone starting fresh, and the DESIGN.md file is the place to look for the transformation passes, though the README warns it is slightly out of date.

The command line help is the other documentation surface, and the README says the --help flag contains a substantial amount of information, pointing at ./krml --help.

Where KaRaMeL is the wrong tool

The first wrong-tool case is general F* code. If your program uses higher-order functions, recursive data types, or a memory model other than the stack and heap one KaRaMeL assumes, it simply is not in the extraction subset, and the restriction is not a configuration option you can relax.

The second case is a project that wants a general purpose verified systems toolchain. KaRaMeL is a back end for one language, one subset, one target language. The paper formalisation relates Low* to CompCert's Clight, which is a research statement about semantics preservation, not a claim of completeness.

The third case is a team that wants readable C from any verified source. The output style is deliberately old-fashioned. The README's own tagline, K&R meets ML, is a description of a design goal rather than a compliment, and readers expecting modern C with clean abstractions will find something else.

For the alternative approach, the difference in approach matters and is worth being concrete about. The realistic alternative for extracting verified code to C is to write the C by hand and use the verification to prove properties about the C itself, which is what a C verification toolchain does. The difference is where the proof lives. In KaRaMeL, the proof is about the F* program, and the C is derived from a proved program, so the C is trusted because the transformation is. In a C verification approach, the proof is about the C directly, so the C is trusted because it was checked.

The KaRaMeL route is more productive when you want to write in a high-level language and the mechanical parts of the C are handled for you. The C verification route is more direct when the C already exists, or when the code has to be shaped in a way that is awkward to express in F*.

There is also a third option worth naming for context: staying in F* and using a verified compiler chain rather than extraction. If the goal is trusted machine code rather than readable C, extraction to C is the wrong destination even when the program is inside the subset.

Licensed under both Apache 2.0 and MIT, with the last release in 2018

KaRaMeL is released under the Apache 2.0 license and MIT license, and the repository carries both LICENSE-APACHE and LICENSE-MIT files. That dual licensing is the standard permissive pairing, and it means you can take the output, and the tool, under whichever terms suit your project.

The release history is the striking part. The recent releases list has a single entry: v0.9.6.0, described as the first official release of KreMLin, dated 2018-05-17. That is the era of the name change, and there are no newer tagged releases in the list.

The last push to the repository was on 2026-10-20, so the tree is being worked on, and the project is clearly not abandoned. But there is no release series to pin to, and the version in the repository comes from the git hash rather than a release tag.

The repository layout reflects a serious research software project. There is DESIGN.md with a technical overview of the different transformation passes performed by KaRaMeL, which the README says is slightly out of date. There is CI.md, Changes.md, a book/ directory, a dune-project, a flake.nix and a .nix/ directory for reproducible builds, and a .odocl directory for documentation. The source is in src/, with krmllib/ holding the runtime library, lib/ for shared pieces, include/ for headers, misc/ for the miscellaneous data the tool needs at runtime, and test/ plus visitors.mk for the test suite and the AST visitor generation.

There is a .clang-format file, which tells you the extracted C is expected to be readable and formatted rather than merely generated, and a .gitmodules file, so there are submodules involved in the build.

The practical advice for anyone picking this up is to build from master, treat it as research-grade tooling, and expect to read DESIGN.md and the ICFP 2017 paper before making changes to the transformation passes.

Editorial conclusion

KaRaMeL suits a team already writing in F* who has proved a first-order program against a stack and heap memory model and needs readable C output, particularly in the verified cryptography space. It does not suit general F* code, since the restrictions on first-order types and non-recursive data types are what the extraction depends on. Before adopting, confirm your F* program satisfies the first-order and non-recursive datatype restrictions, verify that the F* toolchain you have matches the version KaRaMeL expects, and read DESIGN.md, which the README itself notes is slightly out of date.

Frequently asked questions

Official sources

1. FStarLang/karamel on GitHub
2. Issues
3. License: Apache-2.0
4. README
5. Releases