Evergreen: A Provably Safe Systems Language

Evergreen is presented as a systems programming language that combines explicit contracts, checked invariants, and low-level control over memory. Its central idea is to write requirements directly into code - such as a condition that a number must be nonzero - and have the compiler verify them when values are constructed or functions are called. Preconditions, postconditions, and data invariants are framed as obligations rather than comments, with the goal of making safety properties visible and checkable during development.

The language also emphasizes explicit memory layouts, ownership, and borrowed references, with compiler tracking for when memory is live and which uses remain valid. For stronger verification, Evergreen supports proofs, inductive lemmas, and ideal computations; these are erased after checking so they do not add runtime work. The examples illustrate a nonzero type, a simple function contract, mutable borrowing, and proof that a machine value matches an ideal mathematical value. The site positions Evergreen as more powerful than C and safer than Rust, while offering a browser playground and local builds. It also marks interaction with the host environment as an explicit trust assumption, indicating that not every boundary is proven by the language itself.