World model development
as a discipline.
Flyover AI is building the verifiable decision layer for the era of large language models and AI agents — a structured-reasoning platform whose authoring is readable, whose decisions are auditable, and whose API is auto-projected into whatever your downstream systems already speak.
The missing piece is a world model. Make it legible.
The field has converged on the missing piece: a world model, an account of how things stand and how they change under action. Most of the field is building it as a latent space, its meaning read off the network by probing it after the fact. KRML builds it as a representation: its meaning specified in advance, legible to the people who own the decision, and computable underneath. A world you can read is a world you can check.
A policy and a program, written as one document.
KRML is a structured, naturalistic English that compiles, without translation loss, into Answer Set Programming. A domain expert reads it as policy. The compiler reads it as code. The two are the same artifact.
Consider a bank's model-risk policy under SR 11-7. In conventional practice it lives in at least four places: as prose in a governance manual, as decision logic in a validation workflow, as schema in the model inventory, and as monitoring code in the application. Each drifts from the others. Each contains errors the others do not catch. Examiners review them separately and sign off on contradictions.1
KRML collapses the four into one. The KRML in Fig. 1 reads as policy, readable by a model-risk officer or an examiner who has never written a line of code, and is at the same time executable, with formal semantics underneath. The same text carries a definition that classifies models by materiality, a default with its strong exception (a material model lacking independent validation is definitively non-compliant), and a count aggregate (too many material models concentrated in one business line).
Each of these primitives — types with subtype hierarchies, defaults with strong exceptions, definitions with closed-world complement, choice rules, hard constraints, optimization — is a distinct formal device in the Gelfond–Kahl methodology. KRML's contribution is making them all available in a surface syntax that reads as English and lowers to typed-guarded Answer Set Programming.2
- The cost of this drift is borne by compliance teams, by the engineers who maintain the systems, and ultimately by the people the policy is meant to serve.
- See Gelfond & Kahl, Knowledge Representation, Reasoning, and the Design of Intelligent Agents, Cambridge University Press, 2014.
"Model" is a type. Every model has a "materiality", which is a number ranging from 0 to 100. By definition, a model X is "tier-1" if X's materiality >= 70. Normally, a model is validation-compliant. A model X is not validation-compliant if X is tier-1 unless X is independently-validated. ... A business-line X is concentration-risk if X has at least 3 tier-1 models owned by X.
Fig. 1. An excerpt from a KRML model of model-risk governance under SR 11-7: a definition (a closed, materiality-based classification), a default with its strong exception (the validation finding), and a count aggregate (concentration risk by business line). The same source compiles to answer-set programs and is read by a model-risk officer as policy.
The model in Fig. 1 is one of many. See the language worked across a taxonomy of defaults and exceptions, a logic puzzle, and a famous riddle in the Casebook →
Each layer does what it does best.
The pipeline routes the strengths of large language models to the work they are good at, and the strengths of Answer Set Programming to the work it is good at. Neither is asked to do the other's job.
Domain Expert
Holds the policy, the regulation, the rules of the world the system must reason about.
LLM
Translates the expert's prose into candidate KRML, which the expert reviews and refines.
KRML
A signed-off, human-readable model. The authoritative artifact for what the system knows.
Answer-Set Solver
KRML lowers to typed Answer Set Programming; an answer-set solver computes the decisions, and schemas (Protobuf, JSON, SQL) project for the systems downstream.
Decisions
Every decision carries a literal proof chain in English. Auditable by construction.
Determinism on the answer.
Same model and query, the same answer. LLM variability stays in elicitation and narration, never in what is true.
Audit by construction.
A literal proof chain, in English, for every decision. RAG systems show retrieved documents; KRML shows the inference itself.
Foundation-model independent.
Every improvement in LLM elicitation and narration lifts the product without retraining. The lab race is a tailwind, not a threat.
A platform for the systems where verifiability matters.
Flyover AI fits where decisions must be defensible to a regulator, an auditor, a court, or a board — and where the language of the decision must remain legible to the people who own it.
The verifiable action layer for AI agents.
Every agent platform shipping into a regulated, fiduciary, or audit-bearing context will need this layer within twenty-four months. The first credible product to ship has the chance to define the category. Vertical AI startups building structured layers underneath their LLMs — and regulator-facing decision systems satisfying the EU AI Act, SR 11-7, SEC algorithmic accountability rules, and state-level AI laws — face the same structural need.
Forty years of published work, turned into a product.
KRML is not greenfield research. The methodology is published, mature, and production-ready. What did not exist until now was the authoring surface, the engineering-disciplined platform now being built underneath it, and the pipeline that bridges them to large language models.
Built by someone who has been at this for a long time.
Flyover AI was founded by Gregory Gelfond, who has spent the better part of two decades working on knowledge representation and answer-set programming — the formalisms that underpin KRML — and the methodology that makes them coherent as a discipline rather than a collection of techniques.
That work is published, not promised: roughly sixteen peer-reviewed papers and a patent across two decades, in AAAI, AAMAS, TPLP, and the journal of Artificial Intelligence, alongside doctoral work on multi-agent epistemic action languages. It is the same research line — running from Gelfond and Lifschitz's 1988 stable model semantics to the present — that Flint & Steel, an answer-set platform now in active development, is being built to carry forward into a product.
The work of Flyover AI is the work of turning that lineage into a platform — making the discipline of world-model development available to people who do not have decades to spend learning the underlying formalism, while preserving the rigor that makes the formalism worth learning in the first place.
Gregory Gelfond
- ScholarGoogle Scholar
- LinkedIn/in/gregory-gelfond
- Emailgregory@flyoverlabs.ai
