⚖️ Nomos
When the challenge is no longer to answer, but to be true
An LLM can speak about your documents. A rule-based system can tell the truth. But when requirements become maximal — for example in critical industrial contexts (defense, aerospace, certification bodies) — it must sometimes be possible to prove.
Nomos is built on a simple idea: reuse what works in mathematical proof (where correctness is non-negotiable) and hybridize it with what works in industry (RAG, GraphRAG, ontologies), to build systems where truthfulness is not a promise, but an auditable and verifiable property, with industrial-grade guarantees.
Three levels of truthfulness
In industrial applications, we distinguish three levels, in increasing order:
| 💬 Speaking with sources | RAG |
Querying documents, citing passages, and looping through verification —
something people do not always do in practice, even with good methods.
RAG (Lewis et al., 2020) |
| 🕸️ Telling the truth within a rule-defined world | GraphRAG / KG |
A knowledge graph is not “true” by itself: you decide which triples
(subject, predicate, object)are true, and whatever follows by logical inference inherits that guarantee — unlike simple RAG. Defining those truth-bearing triples is a task for human expertise, acting as the guardian of the temple, possibly assisted by LLMs. GraphRAG (Microsoft Research), 2024 |
| ⚖️ Proving mathematically | Proof assistant |
Leveraging advances in mathematical proof for industry.
Here, final validation relies on a logical kernel,
making results auditable and incontestable —
even more strongly than with knowledge graphs.
LeanDojo / ReProver (formal proof + retrieval) Chain-of-Verification (CoVe) |
Nomos: hybridizing so AI proposes and the law decides
The core of Nomos is a strict separation of roles:
- Exploration: a model proposes, organizes, and tests candidates (sentences, triples, arguments, proof steps).
- Control: a verification module decides admissibility — the “judge of last resort”.
In the case of proof assistants, this matches the operational definition: a system that suggests, organizes, and tests, but is ultimately backed by a logical kernel responsible for final validation.
RAG vs GraphRAG: a difference that matters
RAG is excellent for speaking within documents, with sources and verification loops (which we control through experience-based best practices).
GraphRAG becomes relevant when you want to go further: building a world of facts (RDF triples, ontologies, rules), so that outputs inherit a declared-true world. The key idea is simple: it is not “the model” that guarantees truth — it is the control structure (the graph, the rules, and what you decide to treat as true).
What if “proof” left the realm of mathematics?
What makes proof assistants powerful is precisely this combination: heuristic exploration (human or statistical) and formal control that does not compromise.
With Nomos, we aim to transpose this scheme to industrial applications that require strong truth guarantees — where hybridizing RAG, GraphRAG, rules, and proof becomes natural.
In practice, even when we do not “prove” in the strict mathematical sense, we can already strengthen truthfulness by introducing explicit verification loops.
Interested in exploring?
If you have a use case where “answering” is not enough, and where a structured truthfulness pipeline (documents → facts → demonstrations) is required, let’s talk. Nomos is not a chatbot: it is a control architecture, deeply reinforced by mathematical rigor.
Nomos
Pitch sheet in the style of Guy Kawasaki
⚠️ Problem / Opportunity
- RAG is useful, but re-verification is often skipped (truth is not guaranteed).
- Knowledge graphs are powerful, but “what is true” must be made explicit.
- Critical applications require strong truth guarantees, sometimes up to proof.
💎 Value proposition
- A single continuum: “speaking → telling the truth → proving”.
- A clear judge-of-peace model: Right / Not right, explicit and systematic.
- A hybrid architecture: RAG, GraphRAG, rules, and proof assistants when required.
🧪 Secret sauce
- Structured objects (facts, triples, states) instead of free text.
- Explicit admissibility control, separated from LLM exploration.
- When we “prove”, the system operates within a formal framework with a validation kernel.
💰 Business model
- Workshops to design truthfulness pipelines (documents → facts → proof).
- License / integration: on-prem or cloud (setup + support).
- Critical domains: defense, aerospace, compliance, audit, safety.
📣 Marketing
- Storytelling “Nomos”: the law, not magic.
- Demos: same question, three regimes (RAG / GraphRAG / proof).
- Short PoC: private corpus + graph + control loop.
🦅 Competition
- Chatbots and uncontrolled RAG (plausible, but not guaranteed).
- Knowledge graphs without truth governance (links ≠ formal truth).
- Proof tooling disconnected from industrial systems (too “math”, not enough “system”).