Works
A typed operational term-store system for proof-assistant workflows.
MLTTDB, displayed as ML:T:TDB when the wordmark needs the visual rhythm, is a typed operational term store for proof-assistant workflows.
The product idea is deliberately simple:
A table is a type.
A row is a term checked at that type.
In ordinary applications, operational records change frequently while the schema and validation logic are maintained separately. MLTTDB adapts that pattern to proof-assistant-backed systems. Row types and table declarations live in proof-assistant source. Ordered row data lives in a SQLite-backed term store. Validation is delegated back to Agda, Lean, Rocq, or generated proof-assistant source.
The implementation has five main surfaces:
/term-store/v1 for fetching ordered records for one qualified table;The store does not parse or typecheck record bodies. It owns persistence, UUIDs, ordering, database language metadata, and stored table definitions. The proof assistant owns semantic validation.
MLTTDB gives Formal Foundry a path from a checked formalization to operational tooling. A rule or record model can start as proof-assistant source, but the day-to-day data can still be edited through an API or web app. Validation is not lost when data moves out of a static source file.
The most important public explanation is the responsibility split:
| Responsibility | Lives in |
|---|---|
| row types and table declarations | proof-assistant source |
| ordered row data | term store |
| semantic validation | proof assistant or generated source |
schema, tables, data, and eval modes;ff-generics;MLTTDB should be treated as a platform component as well as a product. It is the bridge between static formal schemas and data operations that can actually change.