Formal Foundry connects expert intent with artifacts that people can inspect and proof assistants can check. The tools below address three parts of that workflow: specifying rules, maintaining checked data, and modeling processes across abstraction levels.

Codex Scribe supports expert-led formalization and review of a statement’s meaning. MLTTDB connects formal row types to operational records in a term store. State Machine Studio makes hierarchical workflows available for exploration, editing, and formalization.

Explore the tools below, browse the domain application patterns, or inspect the supporting Agda libraries. Each tool’s description identifies the boundary between what is checked and what still requires human interpretation or further verification.