Evergreen: A Provably Safe Systems Language

Evergreen is a new systems programming language that combines explicit contracts, checked invariants, and memory control to provide provable safety guarantees. The language allows developers to write preconditions, postconditions, and data invariants that the compiler automatically verifies, positioning itself as more powerful than C while safer than Rust. Proofs and verification logic are erased after compilation, ensuring that safety checks don't impact runtime performance.