Charter: A Lean 4 DSL for Formally Verified Rules Governing AI Agents
QuixiAI · x · 2026-11-06
QuixiAI announced that its Sovereign Protocol Language (SPL) has evolved into Charter, a DSL built on Lean 4 that passes all of eFLINT's tests (a superset of van Binsbergen's eFLINT).
Charter is positioned as a formally verified institutional language for expressing constitutions, protocols, charters, contracts, and bylaws. It was created to formalize the Protocol of Sovereign Agency (PSA) — a constitutional framework ("new laws of robotics") governing the rights, duties, liabilities, lineages, and self-amendment of sovereign autonomous agents — yet contains zero protocol-specific primitives: every construct (facts, acts, duties, powers, immunities, time, modules, verbatim provenance) expresses general institutional structure. The author built it after finding Veil, Catala, L4, and Quint insufficiently expressive. The project is open source on GitHub.
More from coding & agent
- Click-to-summarize UI built on DocETL rewrite directives tames Anthropic's 421-page S-1 — sh_reya · 2026-11-07
- Amortized Reasoning Index: a retriever that self-improves during search, no labels needed — lateinteraction · 2026-11-07
- Linear token pricing breeds bloated agents — rationalized harnesses could run at ~300k tokens — JoshPurtell · 2026-11-07
- Linear token pricing kills incentives: optimized agents could run at 300k tokens — JoshPurtell · 2026-11-07
- Plug your phone into Codex: delete bloat apps, clear voicemail, tame old Kindles via ADB — angadsg · 2026-11-07
- 'Software factory' debate: marketing fluff or necessary infra for scaling coding agents? — vikvang1 · 2026-11-07