Codex Scribe
Codex Scribe helps domain experts turn proposed rules into formal statements whose meaning can be reviewed. AI assists with drafting and translation, Agda checks the formal representation, and deterministic readback gives the author a way to inspect what was expressed.
The workflow starts with the expert’s intended statement and a defined vocabulary. Definitions, conditions, exceptions, and assumptions become explicit parts of the formalization rather than remaining implicit in prose.
From a rule to a reviewed statement
- State the intent. Identify the rule, its scope, and the terms needed to express it.
- Develop a formal candidate. Use AI assistance to express that intent within the selected formal setup.
- Check the representation. Agda type checking tests whether the candidate is well formed within that setup.
- Review the readback. Inspect the deterministic reading and decide whether it captures the intended statement. Revise the candidate or its definitions when it does not.
The expert remains responsible for approving meaning. A formal statement can be well typed and still express the wrong rule; making that difference visible is central to the review process.
What the check establishes
Type checking a proposition establishes that it is a valid formal statement under the chosen definitions and assumptions. It does not, by itself, prove that proposition, establish the truth of source facts, or certify a deployed system. Proof construction and operational validation are separate obligations.
The domain portfolios illustrate how this workflow can support review of obligations, eligibility conditions, operating boundaries, and software specifications. They describe application concepts with explicit limits, rather than asserting that each is an available production deployment.
Explore the surrounding workflow
MLTTDB addresses operational records checked against formal types. State Machine Studio addresses layered process models. The Agda libraries provide reusable formalization components, while Blog / Learn explains the relationships between specifications, proofs, solvers, and models.
Book a meeting to discuss a rulebook or workflow and the scope of the formalization it would require.
