Evergreenは、明示的な契約、チェックされた不変条件、およびメモリ制御を単一のフレームワークに統合したシステムプログラミング言語です。実行時のチェックや基本的な型システムのみに依存する多くの言語とは異なり、Evergreenでは開発者がコード内で保持されるべきこと（前置条件、後置条件、データ不変条件など）を記述し、それらの義務をコンパイラに証明させる必要があります。例えば、開発者は非ゼロであることが保証される型を定義でき、コンパイラは、その型に割り当てられるすべての値が構築の瞬間に不変条件を満たしていることを保証します。

この言語の安全性モデルは「証明可能な」コードという概念に基づいて構築されています。これは、依存型と形式的証明の使用を通じて実現され、コンパイラが実行前にロジックを検証することを可能にします。Evergreenの主要な設計目標の一つは、これらの証明が最終的な実行ファイルのパフォーマンスに影響を与えないようにすることです。この言語は、チェックフェーズの後に消去される「理想的な計算」や数学的帰納法による補題を利用します。つまり、安全性を証明するために必要な数学的な作業はコンパイル時に実行され、実行時のコードは軽量で効率的なまま保たれます。

Evergreenは、Rustのような既存のシステム言語に見られる特定の制限に対処することを目指しています。所有権や借用といった概念を採用しつつ、メモリへのアクセス方法においてより高い柔軟性を提供することを目指しています。例えば、Evergreenの開発者は、この言語が「プレーン」と「ノード」のツリーに基づくメモリモデルを使用することで、Rustの借用チェッカーが拒否する可能性のある操作（ベクトル内の2つの可変参照の入れ替えなど）を許可することを意図していると述べています。しかし、このプロジェクトは現在初期の実験段階にあります。ドキュメントはまだ開発中であり、現在の主な焦点は、プロダクション向けのエコシステムやライブラリスイートを構築することよりも、基本的な構文と証明メカニズムの確立にあります。

プロジェクトはまだ初期段階にあるため、実用的な実装に関してはいくつかの疑問が残っています。「プロバー（証明器）」の具体的なロジック（SATソルバに依存するのか、あるいは他の形式的手法を用いるのか）は、まだ公開仕様には十分に詳述されていません。さらに、新しいシステム言語と同様に、Evergreenの長期的な生存可能性は、機能的なライブラリのエコシステムを構築し、既存のツールとの相互運用性を確保できるかどうかにかかっています。これは、プロジェクトの将来にとって依然として未解決の課題です。