Most agent systems let the language model do the reasoning and ask you to trust the result. SynaLemma gives that job to a logic engine. The model writes a rule, and the engine verifies it, computes the answer in your own database and shows you every step.
Built by SynaLinks, a team of CNRS-trained AI engineers who wrote every layer, from the logic engine to the agent.
Which finished bikes stop if Shenzhen VoltPack fails?
All four: Urban S1, Cargo C2, Trekking T3 and Folding F1. Each one needs one of the two battery packs, and both packs use the management board and the casing that VoltPack supplies.
## The assemblies that stop if a supplier fails,
## through every level of the bill of materials.
@OrderBy(SupplierExposure, "supplier_id", "assembly_id");
SupplierExposure(supplier_id:, assembly_id:) distinct :-
Supplies(supplier_id:, part_id: component),
Requires(assembly_id:, component_id: component);
Take a simple question: how much stock of a component is available? Each agent writes valid SQL and returns a different figure, because each one had to guess what “available” means. Does reserved stock count? Do incoming orders? Which site, and on which date? Your plant settled those points years ago, but the agent has no access to the answers.
Nothing fails visibly. The agent returns its figure with full confidence, someone makes a decision on it, and nobody can trace how it was computed. This is the main reason AI projects stall between the demo and production. A larger model has the same problem, because it is guessing the same definitions.
| Agent | Decides available stock is… | Answer |
|---|---|---|
| First | what is on hand | 1,240 |
| Second | on hand, minus what is reserved for work orders | 870 |
| Third | on hand minus reserved, plus purchase orders not yet received | 2,070 |
The agents need your definitions, written down once in a form that a machine has to apply and a person can review. SynaLemma builds that layer and keeps it up to date.
When an agent “explains its reasoning”, you are reading text the model generated after the fact. That text is not a record of how the answer was computed, so auditing it tells you very little. In SynaLemma the model translates your question into a rule, and a logic engine computes the answer from that rule in steps you can replay.
Every rule runs on your real tables before the assistant answers.
The answer quotes the rows the run returned, so nothing comes from the model's memory. SynaLemma runs on your servers with the model you choose, and the assistant is limited to what the role of the person asking allows.
The logic engine makes every inference, and each one can be run again.
Each answer cites its rules, down to the row a figure came from. Your team can open a rule, read it, run it again, edit it or lock it. The rules are files in a git repository, so each change is a commit that records who made it (a person or the assistant), what changed and when.
The first and only AI system that writes its own rules, verifies them formally, and checks their results against mathematical statements.
Every rule passes a formal verifier before any SQL exists, and more than fifteen classes of error are refused with the reason. You then state what a result must always satisfy, in first-order logic, and the engine searches your data for counterexamples. When a rule changes, everything built on it is flagged until it has run again. When you change the model, the rules stay as they are.
No ETL, no second warehouse, no graph database to buy.
Rules compile to SQL and run in the database you already have, on tables that keep their real names, so legacy systems are covered without a migration project. A definition is worked out once and then reused, which saves the tokens a model would spend working it out again. SynaLemma also runs with open models on your own hardware.
Every answer links to a definition like this one. It is short enough for the person who owns the number to read, and precise enough for a machine to verify.
---
name: SupplierDeliveries
description: Purchase orders per supplier, and how many were late.
keywords: [supplier, delivery, late, on time]
---
import tables.PurchaseOrders.PurchaseOrders;
@Assert(SupplierDeliveries,
one_row_per_supplier: "∀ s a b c d, SupplierDeliveries s a b → SupplierDeliveries s c d → a = c",
late_within_total: "∀ s a b, SupplierDeliveries s a b → b ≤ a");
@OrderBy(SupplierDeliveries, "supplier_id");
SupplierDeliveries(supplier_id:, deliveries? += 1, late? += is_late) distinct :-
PurchaseOrders(supplier_id:, is_late:);
A definition from an industrial layer. The statements are written in the notation of the Lean theorem prover and checked against your data. A statement holds when the search for a counterexample returns nothing. This is a check on the data you have, and does not prove anything about data the system has not seen.
Connect SynaLemma to the database you already run (PostgreSQL, BigQuery, Databricks, Trino, Presto, DuckDB, SQLite) or drop in your files (CSV, Excel, JSON, JSONL, Parquet). Databases are queried in place: tables keep their real names and nothing is migrated.
Lemma, the assistant, first looks for a definition that already exists. If there is none, she writes a new rule, verifies it and runs it on your data. She answers only after that, and cites the rule.
The rule is saved with a name and a description. The next question builds on it, and your team can review, correct or lock it.
We have found that the tool alone is not enough, especially for companies with no AI expertise in house. One or more forward-deployed engineers from the team that builds SynaLemma, depending on the size of your project, therefore work alongside your team in a defined role inside the platform.
Most AI products combine someone else's model with someone else's framework. We wrote the framework the agent runs on, the logic engine that verifies its rules, the format that stores the knowledge, and the product that brings the three together. Few teams have built every layer between the database and the model. Because we have, the parts are designed to fit each other, and we can tell you precisely what the system does and where its limits are.
The product your team uses. It runs the three engines on your data and adds the assistant, the rule editor, the dependency graph, roles, and Slack or Teams. A commercial product, under a paid licence, deployed on your infrastructure.
Discover SynaLemmaThe framework the assistant is built with. It holds outputs to a schema, gives agents tools and an embedded sandbox, and optimizes instructions against measured results without touching model weights. Developed under the supervision of François Chollet, the author of Keras. Open source, Apache-2.0.
View on GitHubA logic language with a formal verifier, written in Rust and compiled to seven SQL dialects. What a result must satisfy is stated as a Lean proposition, the notation of the Lean theorem prover, and checked against your data. Open source, Apache-2.0.
View on GitHubThe format your definitions are stored in, with one readable file per concept or rule in a git repository. The history of your reasoning is reviewed and audited like code, and a layer installs from a git repository. Open source, Apache-2.0.
View on GitHubThe model translates and the logic engine reasons. That split is what makes the reasoning auditable and the model replaceable.
See the open-source enginesWhen a wrong figure can cause a production stop or a failed audit, you need to know where each number came from.
Supply chain, purchasing, production and quality teams. Bills of materials, stock, late deliveries and defects each get one definition, shared by planners, buyers and the agents that assist them.
Health, aerospace, energy, finance. Each figure traces back to a rule and to the tables it read, which is what an auditor asks to see.
The demo worked, but nobody would sign off on it. SynaLemma gives the people who must approve it something they can read and check.
The demo takes thirty minutes and is free. Bring a question your teams disagree on, and we will show you SynaLemma's answer and the rule it used. If it is a fit, a readiness assessment comes next, then forward-deployed engineers work with your team.
