Brack is a verified compiler for a subset of Scheme including call/cc, written in HOL4. In order to feasibly achieve complete verification, Brack compiles from Scheme to ML and relies on the verified compiler CakeML for the remainder of compilation to machine code.

Brack uses a continuation-passing style (CPS) transform in its compilation. CPS is a natural program representation which arises from the refunctionalisation of the small-step semantic definition of Scheme, and succinctly captures the behaviour of first-class continuations through the control operator call/cc. This natural representation enables the compiler verification proof for call/cc, making Brack the first verified compiler to support first-class continuations.