NEURO-SYMBOLIC
The model proposes.
Neuro-symbolic AI joins two kinds of intelligence: a that reads and writes like a person, and a that reasons like a mathematician. This page explains both, what an automated formal verification engine is, and exactly where each one sits inside Ironproof.
ARCHITECTURE
01 — Two kinds of intelligence
One learns from examples. The other follows rules to the end.
Each is strong where the other is weak. That is the whole reason to combine them.
The language model
Learns patterns from enormous amounts of text. It understands a messy request, writes code, summarizes a contract, adapts to things it has never seen.
- Strong at
- Language, ambiguity, speed, breadth.
- Weak at
- Guarantees. It is probabilistic: it can be confidently wrong, and it can be talked out of its answer.
The solver
Works on exact rules written in logic. Given a rule and a system, it checks every possible case — not a sample — and gives an answer anyone can re-check.
- Strong at
- Certainty. Its answer holds over every case in the class it was asked about.
- Weak at
- Reading the world. It needs the question already written precisely.
02 — Neuro-symbolic
Let the model be creative.
A neuro-symbolic system puts each part where it is reliable. The neural side handles language: it proposes an action, a translation, a candidate answer. The symbolic side checks it against rules that were fixed in advance, and only the symbolic side can say yes.
The order matters. A model that grades another model is still a model — it can be prompted, persuaded, or simply wrong. A solver cannot be argued with: either the rule holds in every case, or it hands back the exact case where it breaks.
Intelligence without proof is a guess. Proof without intelligence never leaves the lab. Together, they ship.
03 — The engine
What an automated formal verification engine is.
Formal verification means proving, with mathematics, that a system obeys a rule — for all inputs, not the ones you happened to test. For decades it required specialists writing proofs by hand, which is why it stayed in aerospace, chips and cryptography.
Automated means the engine does that work itself. We use Z3 and its Spacer engine: you give it the rule and the system, and it searches for a proof — including the inductive invariant, the property that stays true at every step — or for a counterexample. No mathematician in the loop. A solver can return three kinds of answer:
No case breaks the rule.
Not “we didn’t find one.” The solver shows none can exist — the technical word is UNSAT, unsatisfiable.
Here is the exact case.
The inputs, the state, the step where the rule fails. Concrete enough to replay and fix.
Not settled.
Some questions are too hard to close in the time given. Undecided is not a pass, and an honest system never counts it as one.
04 — How it fits together in Ironproof
From a proposed action to a proof you hold.
One engine, the same steps on every surface. The model can only ever appear in the first one.
- 01 · PROPOSE
An AI agent asks to act
A refund, a payment, an access grant, a deployment. The request may come from a model — that is the neural part, and it is where mistakes and manipulation start.
- 02 · COMPILE
Your rule becomes logic
Your policy is compiled once into the form the solver reads and the form the runtime enforces. One compiler, so the two cannot quietly disagree.
- 03 · PROVE
The engine decides
The solver proves the rule holds across sequences of actions, or returns the counterexample. At run time every action is checked against that same compiled rule, and nothing executes without a passing decision.
- 04 · RE-CHECK
Don’t trust the search
The invariant the solver found is re-checked in a fresh solver before anything is sealed. Finding a proof and checking it are kept apart on purpose.
- 05 · SEAL
Post-quantum record
The decision and its proof are hash-chained and signed with Ed25519 and ML-DSA-65 (FIPS 204). Any later edit is detectable.
- 06 · VERIFY
Offline, without us
Your auditor re-checks the sealed record with an independent verifier, without ever contacting Ironproof.
05 — Where the model sits, exactly
On the decision path,
The production path that authorizes an agent's action calls no language model at all. In our research tribunal, a model may read the request and give its opinion on intent — that opinion is recorded in the sealed record and never counted. The same request, in the same state, under the same policy, gets the same verdict whether the model agreed, disagreed, or was unreachable.
The decision itself is made by evaluating your rules, and that shortcut is licensed by a theorem checked in Lean 4: deciding by evaluation and deciding by the solver give the same answer for every policy and every action. The neural side brings understanding. The symbolic side keeps the final word.
06 — What it does not do
The limits, stated up front.
A proof is only as good as the rule.
The engine proves your system obeys the rule you wrote. Whether that rule says what you meant is a human question — today it is the hardest part of the work, and we do it with you.
Proven within a class, not everywhere.
Each proof covers a precisely stated class of actions and rules. Outside that class, it says nothing — and the record states the boundary.
We don’t make the model safe.
A compromised or confused model can still ask for the wrong thing. We make sure it cannot get it unless the rule allows it. Hardening the model itself is separate work.
07 — Glossary
The words, in one line each.
- A model that learns patterns from data. Language models are neural networks.
- Computation on explicit rules and logic, where every step can be checked.
- A system that combines both, each where it is reliable.
- A mathematical proof that a system obeys a rule for every input.
- The engine that decides whether a logical formula can be satisfied. Z3 is one.
- “Unsatisfiable”: no case violates the rule. The answer a proof rests on.
- A concrete case where the rule breaks.
- A property true at the start and preserved by every step — so true forever.
- A signature designed to stay unforgeable even against future quantum computers.
NEURO-SYMBOLIC
See the engine on one of your workflows
Pick one action your agents take. We write the rule with you, prove it, and hand you the record.