Other agent systems rely on the language model to reason. SynaLemma is a harness built the other way round: the model translates your question into a rule, and a logic engine does the reasoning. It verifies the rule formally, derives the answer in the database you already run, and keeps the rule, so every step can be read and replayed.
Most agent systems put the language model in the middle and let it reason its way to an answer. SynaLemma puts it at the edge. The model proposes a rule, and the engine performs every join, recursion and total. Nothing reaches your data or your answer without going through the engine.
The model reasons in text. Its “explanation” is written after the fact and is not a record of how the answer was computed, so there is nothing to replay.
The model translates your question into a rule and words the answer. Every inference in between is the engine's, and can be replayed.
Each layer has one job and passes the next layer something it can check. Three of them are open source; the fourth is the product that assembles them.
What your team uses: Lemma, the assistant; tables, concepts and rules you can read and edit; the graph of what depends on what; roles, history, and the channels you already talk in.
Drives the model step by step: searches existing definitions, decomposes the question, writes rules, calls tools. Outputs are held to a schema, the model can be swapped, and every step is traced.
Verifies each rule before any SQL exists, compiles it to the SQL dialect of your database, and checks what its result must satisfy against your data.
Where definitions live: one readable file per table, concept or rule, in a git repository. A layer is reviewed like code and can be installed in another project.
Your model · local or hosted, replaceable
The agent searches the layer for a definition that already answers the question. A layer of thousands of definitions never goes into the model's context whole: only what matches does.
If none fits, it writes one, building on the concepts already there instead of starting from raw tables.
The rule goes through the formal verifier. If it does not check, it is refused with the reason, and nothing is saved unless the whole layer still holds together.
The verified rule is compiled to SQL and executed in your database. Its assertions are checked on the same data.
Only then does the assistant answer, quoting the rows the run returned and citing the rule, which you can open.
The rule is committed to the layer with its author and date. The next question starts from it.
Asking a second model to check the first one only adds another opinion. SynaLemma checks with logic instead. It is the first and only AI system that writes its own rules, verifies them formally, and checks their results against mathematical statements.
Synalog's formal verifier examines every rule before any SQL is generated, with no database involved: variables that are never bound, unsafe negation and aggregation, negation through recursion, recursion without a base case or a bound, unknown columns, functions and predicates. More than fifteen classes of error, all reported at once. A rule that does not check is never saved and never run.
An assertion states what a result must satisfy, independently of how it is computed: a part appears once, a stock is never negative, late deliveries never exceed deliveries. It is written in first-order logic (∀, ∃, →, sums and comparisons) as a Lean proposition, the notation of the Lean theorem prover. Synalog compiles a search for counterexamples to SQL and runs it on your database. In SynaLemma a broken assertion shows on the rule, with the rows that break it one click away.
✗ OnTimeDelivery.meets_service_level is violated:
∀ s r d t, OnTimeDelivery s r d t → t ≥ 0.6
2 counterexamples:
+-------------------+------+----+-------+
| s | r | d | t |
+-------------------+------+----+-------+
| Shenzhen VoltPack | high | 34 | 0.588 |
| Hsinchu Controls | high | 47 | 0.553 |
+-------------------+------+----+-------+
Auditing an AI usually means reading logs of what a model said. In SynaLemma you audit two exact records: the derivation, made by the logic engine, and the history of the rules, kept in git, the tool software teams already use to track every change.
Each figure cites its rule and the row it came from. Each rule names the concepts it builds on, and each concept the tables it reads. Follow the chain, or run any link of it again.
A semantic layer is a git repository: one file per table, concept and rule. Every change is a commit attributed to its author, whether a person, Lemma or another agent, with the difference and a way back.
What was this definition on the day that figure was reported? Who changed it, and when? Compare two versions, restore one, or put a change through the same review as any other code.
The history records your definitions and how they changed, not your data: the rows stay in your database.
A classic semantic layer is a modelling project that takes months and is out of date soon after delivery. SynaLemma writes the layer as questions are asked, on top of your existing databases.
Rules compile to SQL and run where the data is. On a database you operate, SynaLemma declares the tables you choose and never changes them. A read-only account is enough.
Old schemas keep their real table and column names, spaces and accents included. The layer gives them a meaning without touching them.
Entities and relationships are modelled over your relational tables. The graph is virtual: it compiles to SQL.
Bills of materials through every level, reporting chains, “which assemblies stop if this supplier fails”: recursion to a depth you declare, so it always terminates, and reasoning over time.
And your files: CSV, Excel, JSON, JSONL, Parquet.
The layer belongs to you. Anything the assistant writes can be read, corrected and locked by a person.
SynaLemma is deployed on your infrastructure. With a local model, nothing leaves it. With a hosted model, your questions and the data excerpts needed to answer them go to the provider you chose, and nowhere else.
Open models on your own hardware (Ollama, vLLM, LM Studio) or the provider you already have a contract with. The rules do not depend on it.
Queried in place, through an account that only needs to read. Database credentials are stored encrypted. Voice messages recorded in the app are transcribed on your server.
Plain files in an open language, on engines published under Apache-2.0. They also run with the open-source tooling alone.
No. SynaLemma comes with one or more dedicated forward-deployed engineers, depending on the size of your project, from the team that builds it. They work alongside your team to deploy it, handle your data, and write and verify your definitions with your experts.
It decides what to ask the engine: which concepts to combine, and how. That decision is written down as a rule you can read, and the engine, not the model, derives every row from it. If the decision is wrong, it is wrong in a place you can see, correct once, and lock.
The three engines it is built on (Synalinks, Synalog, Semantic Layers) are open source under Apache-2.0. SynaLemma itself, the product that assembles them, is proprietary and sold under a commercial licence. Your rules are files in the open format, so they are never locked in.
PostgreSQL, BigQuery, Databricks, Trino, Presto, DuckDB and SQLite, queried in place: your tables stay where they are. And files: CSV, Excel, JSON, JSONL and Parquet. One rule compiles to the SQL dialect of whichever engine it runs on.
Any model that supports tool calling, chosen from a catalogue in the settings: open models served locally through Ollama, vLLM or LM Studio, or hosted providers such as Mistral, Anthropic, OpenAI or Google. Changing model does not change the rules. Everything except the conversation itself works with no model at all.
A structurally wrong rule is refused by the verifier. A rule that contradicts an assertion is flagged with the rows that break it. And because the rule is readable, the person who owns the number can see it and correct it. That is not possible when the answer is a paragraph of prose.
No. SynaLemma draws no charts: answers are figures, tables and the rules behind them. It gives the definitions behind your dashboards one place to live, and lets people and agents ask questions in plain language against them.
In a free thirty-minute demo, we show you SynaLemma's answer and the rule it used.
