Evergreen claims a systems language that is provably safe and faster than C

Evergreen: A Provably Safe Systems Language

Evergreen puts preconditions, postconditions, and data invariants directly beside the code they describe, turning them into obligations the compiler must check. It tracks explicit memory layouts, ownership, and borrowed references, and erases proofs, inductive lemmas, and ideal computations after verification so runtime performance stays intact. The project bills itself as more powerful than C and safer than Rust, with a WebAssembly playground that runs locally in the browser.