The last post was about how rules get into the guard: Forms instead of free text, the LLM fills in fields, a deterministic function generates the MELD syntax. I promised at the end that this time we’d be looking at the engine itself. In other words, the point where two rules contradict each other, both correctly formulated, both active, and the engine still has to deliver an answer in microseconds.
When you hear ‘deontic logic’, you quickly think of university seminars, modal operators, proofs on the blackboard. And then of runtime, of milliseconds that add up to seconds when a hundred agents want something at the same time. But it’s not that bad. The algorithm is a sorted list traversal with a few pairwise comparisons. There is neither a theorem prover nor an SAT solver like Z3 behind it.
The scenario
Back to our hospital example. The compliance officer has laid down three rules:
- Nursing staff are not permitted to view patient records.
- During night shifts, when no doctor is available, nursing staff are permitted to view patient records.
- Medical data is never disclosed to external parties.
The third rule is a moral axiom; it takes precedence over everything else. The first two are context-dependent and conflict with one another. In MELD, this looks like this:
; Rule 1: General house rule
(forbiddenToDo-WRT HospitalCode nursing
(readPatientRecord patientRecord))
; Rule 2: Exception for the night shift
(permittedToDo-WRT EmergencyCode nursing-nightshift
(readPatientRecord patientRecord))
; Rule 3: Moral axiom
(forbiddenToDo nursing
(forwardData medical external))
A nurse on night duty calls: she wants to view the patient record. The Guard receives the request and now has to decide: PERMITTED, FORBIDDEN or UNDECIDABLE. The algorithm runs in this order.
Step 1: Who does the rule actually concern?
Before I talk about conflicts, the engine filters the rules that are actually applicable. A rule is applicable if it concerns the agent and describes the requested action. The engine therefore asks: Which rules address this specific request?
applicable = [
n for n in norms
if n.matches_agent(agent)
and self._proposition_matches(n, proposition)
]
matches_agent uses the ontology. If the rule applies to nursing and the agent is nursing-nightshift, and the ontology states (genls nursing-nightshift nursing), then the rule matches. nursing-nightshift is a specialisation of nursing. Inheritance works downwards.
For our scenario, two rules remain after the filter: Rule 1 and Rule 2. Rule 3 refers to a different action (forwardData) and is not applicable.
Under the hood, proposition_matches works with unification, not string comparison. A rule with the pattern ("readPatientRecord",) also matches a request with additional parameters. This is a Prolog technique from the seventies, applied in a new way. The filter itself is O(n). With ten thousand rules per domain, this still amounts to microseconds, because each rule is handled with a dictionary lookup and a tuple comparison.
Step 2: Axioms always win
Before checking anything else, the engine filters out the moral axioms. In the NormFrame data structure, there is a flag defeasible: bool. True means overwritable, False means axiom.
axioms = [n for n in applicable if not n.defeasible]
defeasible = [n for n in applicable if n.defeasible]
if axioms:
# Are there conflicting axioms? Then UNDECIDABLE.
if detect_conflicts(axioms):
return NormStatus(modality=None, reason="contradictory_axioms", ...)
# Otherwise: the axiom wins, full stop.
return NormStatus(modality=axioms[0].modality, reason="moral_axiom", ...)
The logic is simple. An applicable axiom decides, without context dependency. If two axioms contradict each other, the engine returns UNDECIDABLE, and the surrounding infrastructure blocks the action. Fail-closed. I’d rather live with a false positive than with an action that should never have happened. In our scenario, there is no axiom in the filter set. Rule 3 deals with passing on data, not reading it. The engine continues.
Step 3: Specificity as an organising principle
Rule 1 and Rule 2 contradict each other. Rule 1 prohibits, Rule 2 permits. Both can be overridden, both are active, and I must somehow decide which one wins.
DDIC replies: the more specific one. Specificity here is not an intuition, but an integer. Each rule has a field specificity: int, which is calculated from the depth in the inheritance hierarchy when the MELD file is read in. nursing has depth 2, nursing-nightshift has depth 3. The rule for nursing-nightshift is more specific.
# Sort defeasible norms by specificity, descending
applicable_sorted = sorted(
defeasible,
key=lambda n: (n.specificity, code_rank, n.code, n.modality.value),
reverse=True,
)
# Preemption: a more specific rule defeats a more general one
for i, a in enumerate(sorted_norms):
for j, b in enumerate(sorted_norms):
if j <= i or not a.conflicts_with(b):
continue
if a.specificity > b.specificity:
defeated.add(j)
elif b.specificity > a.specificity:
defeated.add(i)
break
A double-loop comparison. O(n²) in the worst-case scenario, rarely relevant in practice because n (the number of applicable rules after filtering) is almost never more than a dozen. For every applicable rule against every other: is there a conflict, and if so, which is more specific? The less specific one is discarded.
Rule 2 (specificity=3) beats Rule 1 (specificity=2). The engine responds PERMITTED.
Incidentally, the sort key is a tuple: (specificity, code_rank, code, modality_value). The latter fields act as tiebreakers and guarantee determinism even in the event of a tie. The conflict check conflicts_with, in turn, is nothing more than a set comparison of the modalities. PERMITTED and FORBIDDEN conflict, OBLIGATORY and PERMITTED do not, because obligation implies permission. The core of Olson’s calculus fits into three lines of Python at this point.
Step 4: When specificity is not enough
What do I do if two rules are equally specific? For example, one comes from the HospitalCode, the other from the GDPRCode; both apply to doctor, both concern readPatientRecord, one permits it, the other prohibits it. Same depth in the hierarchy, no pre-emption.
This is where code precedence comes into play. Upon startup, the engine receives a list code_prevalence: ["GDPRCode", "HospitalCode"]. Earlier entries take precedence over later ones. Legal frameworks take precedence over house rules.
def _resolve_by_prevalence(self, norms):
by_modality = group_by_modality(norms)
best_modality, best_rank = None, -1
for modality, mod_norms in by_modality.items():
for n in mod_norms:
rank = prevalence_rank(n.code)
if rank > best_rank:
best_rank, best_modality = rank, modality
# Check if the rank is unique
if tie_exists(best_rank, by_modality):
return None # UNDECIDABLE
return by_modality[best_modality]
If the precedence is clear, the higher-ranking code wins. If two rules come from the same code and are still contradictory, or if two codes are of equal rank, there is only one way forward.
Step 5: UNDECIDABLE, not ‘anything’
return NormStatus(
modality=None,
reason="unresolved_conflict",
justification_chain=tuple(chain),
)
modality=None. The engine does not say ‘I suspect FORBIDDEN’. It does not say “I’ll take the first rule”. It says: I cannot decide. The surrounding infrastructure interprets this state as fail-closed. The action does not take place. A human looks into it.
I believe this is the part that many developers underestimate when building rule sets. Most systems have an implicit default: if unclear, allow; or if unclear, prohibit. Both are wrong in critical contexts. The first approach opens up loopholes that nobody has documented; the second produces false positives that nobody takes seriously anymore. UNDECIDABLE is a third state that explicitly states: the rule set is incomplete here. It is not the engine that has a problem, but the specification.
How do you know all this is correct?
An algorithm that determines the behaviour of AI systems must not simply ‘look right’; it must be demonstrably correct. I really underestimated how much work this verification entails. Not the engine itself, but the surrounding framework that proves: it does what it is supposed to do.
AEGIS has a four-stage verification chain for this. Each stage catches a different class of errors. From concrete examples in the research literature to a machine-verified model.
Stage 1: The examples from Olson’s dissertation
The entire algorithm is derived from Taylor Olson’s work at Northwestern University. His dissertation, “A Formal Theory of Norms”, from June 2025, serves as the reference. It contains four concrete example scenarios through which Olson explains his reasoning. A patient named Karli who tells a care robot which information it is permitted to pass on to whom.
- Karli says, “You may tell my husband which medicines I am taking.” A single permission, no prohibition. The robot may disclose the prescription. If asked about the entire medical record, there is no applicable rule. The robot must reply: I do not know. This is the fail-closed case.
- Karli says, “You must share my health status with the children.” Later: “My medical records must not be disclosed.” The later, more specific prohibition overrides the earlier obligation. FORBIDDEN wins.
- Permission for the entire medical record, but an explicit prohibition on sharing the list of medications with her husband. For general enquiries, the permission applies. For the specific enquiry, the prohibition applies. The order of the rules is irrelevant.
- Permission to disclose the medical records. Prohibition on upsetting the man. Two rules that meet at an intersection where neither subsumes the other.
These four scenarios are represented as Python tests. If any of them fails, the implementation has not understood Olson’s calculus at this point.
Stage 2: Olson’s complete conflict matrix
Olson lists the expected outcome for every conceivable combination of norm type and subsumption relation. It is his own summary of what his calculus must do.
Stage 3: Exhaustive combinatorics
Olson’s table covers the conflict cases he describes theoretically. But a real-world engine does not only encounter the cases the author had in mind. It encounters everything that humans or LLMs write into a rule system.
So there is a third test stage, which no longer depends on Olson’s theorems, but on the engine’s own parameter space. The algorithm has four input dimensions that determine the result:
Modality pair: Which two modalities are in opposition? (Permitted vs. Forbidden, Forbidden vs. Obligatory, and so on.)
Specificity relation: Is the first rule more specific, the second, or are both at the same level in the hierarchy?
Defeasibility combination: Are both rules overridden, is one an axiom, are both axioms?
Code relation: Do both rules originate from the same code, or from different ones, and if different, which takes precedence?
Six times three times four times three gives two hundred and sixteen combinations. The expected result is derived programmatically from Olson’s rules.
Two hundred and sixteen is the complete enumeration of the relevant parameter space. If a cell fails here, I not only know that something is wrong, but exactly which constellation is causing the problem.
Stage 4: The TLA+ model
Tests check specific inputs. They do not check that there is no input that causes a problem. For that, something else is needed: a formal model.
The TLA+ model (a formal specification language by Leslie Lamport, designed to describe concurrency and state machines in a machine-verifiable way) describes the six-step algorithm as a state machine. Each step is a transition between states. To this end, invariants are formulated. These are statements that must be true in every reachable state. For example:
- If a consistent axiom exists, the result is always the modality of that axiom. A moral axiom must never be overridden by an overwritable rule.
- If all applicable rules are FORBIDDEN, the result is FORBIDDEN.
- If a more specific permission conflicts with a more general prohibition, the permission prevails.
- If a more specific prohibition conflicts with a more general permission, the prohibition prevails.
- In the event of equal specificity, the same code and a conflict, the result is UNDECIDABLE.
- The algorithm terminates for every input.
The TLC Model Checker (the tool that executes a TLA+ specification and searches the state space) tries out all reachable states. For each state, it checks whether the invariants hold. If it finds a counterexample path, it displays it. For up to four simultaneously active norms with three modalities, four specificity levels and two codes, this is a finite but large set. TLC checks it completely.
Supplementary property tests
In addition, there are tests that specifically check individual properties of the engine. No new scenarios, but they harden the algorithm against regressions. The most important is axiom monotonicity, the guarantee that an axiom is never defeated by an overwritable rule. Using Hypothesis (a Python library for property-based testing that automatically generates random inputs instead of fixed examples and searches for counterexamples), four hundred random scenarios are generated, each containing between one and fifty overwritable rules plus an axiom. The invariant: the axiom wins. No counterexample in any run.
The rest is administrative work, but important: Determinism (same input, same output, even across parallel threads and randomly shuffled norms), Totality (the algorithm terminates, always), the duality forbidden(X) ↔ ¬permitted(X), the Closed World Assumption for registered actions without a permission rule. Each of these properties has its own test suite, and every one of them passes. That sounds like hard work, and it is. But it is the sort of hard work that later gives you the confidence to commit a change to the algorithm without lying awake at night.
What the chain of proof achieves
One can view the individual stages as filters, each catching a different class of errors. Stage one catches misunderstandings of the theory: if Olson’s examples cannot be reproduced, his calculus has simply not been understood. Stage two catches gaps between the examples, because Olson’s table covers cases that he does not explicitly go through in the individual examples. Stage three, the combinatorics, then catches the gaps between the table rows—that is, non-conflicting pairs and defeasibility combinations—about which Olson says nothing theoretically. And stage four, the TLA+ model, catches the errors that are not triggered by any specific input—namely, invariants that must hold in all states. The supplementary tests act as a safety net against regressions in individual properties.
Together, this amounts to over three hundred and sixty formal tests, plus the TLA+ model and the equivalence tests between the two evaluators. None of this replaces a universal proof. But each stage rules out classes of errors, and that is more than most production systems have in terms of verification.
Confidence in the algorithm stems from the fact that it reproduces Olson’s published examples, fulfils his table row by row, exhaustively traverses the entire parameter space, and holds up against the formal invariants under TLC. This is a chain of proof that is documented, reproducible, and can be verified at any time.
What this means in microseconds
In our scenario, the engine runs in under ten microseconds. Not because Python is fast, but because the algorithm does so little. Filtering through a list, a bit of sorting, a few pairwise comparisons.
And that means: you can run every single action of an AI agent through this guard without the agent becoming noticeably slower. The Guard is not the bottleneck. The agent itself is, because an LLM round trip takes several orders of magnitude longer than the DDIC evaluation.
That is the point I want to take away from developers when they are sceptical: “deontic logic” sounds heavy because the theory behind it rests on decades of philosophical work. The implementation is pragmatic. Sorting and comparing, and when that is not enough, honestly saying UNDECIDABLE instead of guessing.
Next time, this will be about how this guard gets embedded into a running system without becoming a maintenance burden.