Facet
A modern, themeable IDE for the formal verification era.
Refracting code, proofs, and conversation into one cohesive light.
Vision
Facet is a "Magical Girl" IDE for Lean 4. It combines the speed of a Rust-based editor, the modularity of a modern browser, and the social depth of a Discord community.
Features
⚡ Rust + Webview
A hybrid architecture. The core text editor is C++ (for zero-latency typing), while the Proof View is a detachable webview for rich interactivity.
💬 Social Coding
Proof Rooms: Jump into a file and instantly join its voice/chat channel. Anchor discussions directly to specific proof states, not just lines of code.
💎 Transformation Modes
Switch between "Code Mode" (raw syntax) and "Tactic Mode" (interactive card battles). Gamified mastery tracks guide you from novice to expert.
🌈 Radiant UI
Fully themeable with a "Magical Girl" default aesthetic. Bright, fun, and energetic— because formal logic doesn't have to be gray.