Your Domain Knowledge.
Formally Proven. Automatically.
Koda is an AI-powered ontology engine that converts your regulatory documents into formal knowledge graphs, detects logical contradictions with mathematical certainty, and provides Glass Box reasoning: not probabilistic explanations, but provable proofs.
AI Without Domain Reasoning
Organizations in regulated industries process thousands of documents containing complex, interrelated business rules. Insurance filings, healthcare protocols, financial compliance frameworks, legal contracts. Every document adds rules. And those rules interact, sometimes in ways nobody expects.
Do any of your rules contradict each other? Not 'if they might conflict'. But do they logically contradict and can you prove it?
What gaps exist in your coverage? Not what you think you covered. What is provably missing from your rule set?
Can you explain the reasoning? Not with a confidence score. With a formal proof that a regulator can independently verify.
How long does it take to find out? Days of manual review? Weeks? Or five minutes?
Today, finding contradictions in regulatory documents is a manual, expert-intensive process. Actuaries, underwriters, compliance analysts read documents, build mental models, and hope they catch the conflicts. They are good at it. But they miss things. Not because they are careless, because formal logic at scale exceeds what someone's working memory can hold.
Koda replaces hope with proof.
The Three-Stage Pipeline
Koda takes natural language documents and transforms them into formal OWL ontologies, structured knowledge graphs where every concept, relationship, and constraint is machine-readable and logically verifiable. Not pattern matching. Not statistical inference. Formal logic, the same mathematical framework used in theorem proving.
Concept Extraction
The Insurance Ontology Architect
Koda reads your document and extracts domain concepts: classes, properties, entities, relationships. A rate filing becomes a structured set of coverage types, eligibility criteria, property classifications, and underwriting rules.
Axiom Generation
The Logic Engineer
Extracted concepts are transformed into formal OWL axioms, logical statements that encode your business rules in a mathematically precise format. 'Properties with foreclosure history are ineligible for coverage' becomes a formal class restriction.
Collision Detection
The Reasoner
The complete axiom set is loaded into an OWL 2 Description Logic reasoner (HermiT). The reasoner checks the entire ontology for logical consistency, not by sampling, not by estimation, but by formal proof.
What Koda Finds
Koda detects three types of logical problems, each with a formal proof.
Mutual Exclusivity Violations
Two rules that cannot both be true at the same time.
A rate filing states "All foreclosure properties are excluded from coverage." A separate section states "All properties under $500,000 are automatically eligible." A foreclosure property worth $400,000 satisfies both rules, but they contradict.
Semantic Inconsistency
The same term used with conflicting definitions.
One section defines "heat pump" as central heating. Another classifies "heat pump" as supplemental heating. If central and supplemental are mutually exclusive categories, this is a semantic inconsistency.
Subsumption Conflicts
Illogical parent-child relationships in the classification hierarchy.
Multi-owner properties classified as both "eligible with conditions" and "ineligible" in the same hierarchy. The subclass cannot contradict its superclass.
Human reviewers working through a 200-page filing often miss these because the conflicting statements are in different sections, written by different authors, at different times. Koda catches them in under a second.
Proofs, Not Predictions
When ChatGPT or Claude analyzes a document and says "there might be a conflict between section 3.2 and section 7.1," that is a prediction. It is useful. But it is not proof. A regulator cannot independently verify it.
When Koda detects a collision, it produces a formal Description Logic proof that traces the exact chain of reasoning. This proof is deterministic. Run it again tomorrow and you get the same result. Hand it to a third-party auditor with an OWL reasoner and they can independently verify it.
"Solve the analyst concern of 'We think there is a problem.' To, we can prove there is a problem and we can prove why."
Axiom A states: ForeclosureProperty SubClassOf ExcludedProperty
(Section 3.2, page 14)
Axiom B states: Under500KProperty SubClassOf EligibleProperty
(Section 7.1, page 42)
DisjointClasses(ExcludedProperty, EligibleProperty)
(Domain constraint)
ForeclosureProperty AND Under500KProperty is UNSATISFIABLE
(QED - Formal proof)
Three-Layer Ontology
Koda organizes domain knowledge into three composable layers. This architecture is domain-agnostic, the layers apply to any regulated industry.
Domain Foundation
Industry standards and universal definitions. In insurance, this is ACORD codes and standard coverage types. In healthcare, HL7/FHIR. In finance, Basel III. In manufacturing, ISO standards.
Changes slowly and is the bedrock the entire industry agrees on.
Jurisdiction / Regulatory Scope
Regulatory requirements specific to a jurisdiction, authority, or governing body. California homeowners rules differ from Texas rules. State Medicaid requirements differ by state.
Changes at the pace of regulation.
Organization-Specific
Your company-specific rules, products, and policies. Carrier-specific underwriting guidelines, custom coverage endorsements, and proprietary risk models.
Unique to each tenant. Grows with every document ingested.
Each layer imports the one below it. Your organization's rules (Layer 3) are validated against jurisdictional requirements (Layer 2), which are validated against industry standards (Layer 1). A collision at any layer is detected and reported.
The three-layer architecture adapts. The reasoner does not care what domain the axioms describe.
From Document to Proof
Here is what a typical document analysis looks like, end to end.
Submit Your Document
Send your regulatory document to Koda via MCP. For large documents, use the async pipeline for non-blocking processing with job polling.
{
"jsonrpc": "2.0",
"method": "tools/call",
"params": {
"name": "ingest_requirements_document",
"arguments": {
"content": "California Homeowners Rate Filing HO3...",
"ontology_ref": "data/ontology/homeowners-renters.owl"
}
}
} Koda Processes the Document
The three-stage pipeline runs automatically behind the scenes.
Review Results
Receive structured results with extracted concepts, generated axioms, detected collisions with formal proofs, and identified coverage gaps.
{
"status": "success",
"concepts_extracted": 541,
"axioms_generated": 550,
"collisions": [{
"collision_type": "mutual_exclusivity",
"severity": "CRITICAL",
"explanation": "ForeclosureProperty is both excluded and eligible",
"proof": "SubClassOf(ForeclosureProperty, ExcludedProperty) AND ...",
"source_sections": ["Section 3.2 (page 14)", "Section 7.1 (page 42)"]
}],
"coverage_gaps": [
"No wind/hail deductible for coastal zones",
"Missing earthquake endorsement for fault-adjacent properties"
],
"reasoning_time_ms": 487
} Targeted Validation
Run targeted collision checks on specific rule pairs without processing an entire document. Validate business terms against your ontology.
{
"name": "detect_collision",
"arguments": {
"axiom_a": "All foreclosure properties are excluded",
"axiom_b": "All properties under $500K are eligible",
"ontology_ref": "data/ontology/homeowners-renters.owl"
}
} Integrate with Axis
Register Koda as a governed step in your Axis pipeline. Axis handles governance, telemetry, and audit trailing automatically.
Governed by Axis
Koda operates as a standalone service, but its full power emerges when integrated with Axis, the governance orchestration platform. In an Axis pipeline, Koda runs as a governed step with full audit trailing and telemetry capture.
When Koda detects a collision during an Axis orchestration, the transaction parks, the proof is sealed into the immutable audit trail, a human analyst is notified, and the collision appears in the Glass Box Dashboard.
On Collision Detection
steps:
- step_name: classify
agent: internal://document-classifier
required: true
- step_name: ontology_mapping
agent: internal://koda-ontology
required: true
input_from: steps.classify.output
- step_name: validate_rules
agent: internal://drools-validator
required: true
input_from: steps.ontology_mapping.output 
Figure 1: Koda Processing Flow - From Document Input to Collision Proof
Three-Tier Data Scrubbing
Before any LLM processes your document, Koda applies three tiers of data scrubbing. Sensitive data never reaches the LLM.
Ontology concepts are extracted from scrubbed text. Formal axioms reference domain concepts, not personal data.
Real Numbers From Real Documents
Koda is not a prototype. These are results from processing actual regulatory filings.
Accuracy Benchmarks
MCP Tools, SDK, and Integration
import httpx
response = httpx.post(
"http://koda.novus-forge.com/mcp",
json={
"jsonrpc": "2.0",
"method": "tools/call",
"params": {
"name": "detect_collision",
"arguments": {
"axiom_a": "Foreclosure excluded",
"axiom_b": "Under $500K eligible"
}
},
"id": 1
}
)
collision = response.json()["result"]
print(f"Detected: {collision['detected']}")
print(f"Proof: {collision['proof']}") {
"mcpServers": {
"novus-koda": {
"command": "python",
"args": [
"-m", "koda_mcp.server"
],
"env": {
"GEMINI_API_KEY": "..."
}
}
}
} Add Koda to Claude Desktop for conversational access to all 7 MCP tools. Detect collisions, validate terms, and process documents through natural language.
Koda runs as a Tier 3 (Verified) internal agent within Axis, but its capabilities are not
hidden behind a proprietary wall. Koda publishes an A2A Agent Card at
/.well-known/agent.json,
advertising its ontology mapping, collision detection, and term validation skills to any
A2A-compatible system. Its capabilities are also registered in AOW-compatible terms,
so external callers can discover Koda through Axis's agent registry.
Direct invocation still goes through MCP. But discovery is open.
See the Full Use Case
1,429 concepts, 1,782 axioms, 78 collisions detected from a real California HO3 filing
See Koda in Action
Request a demo to see how Koda transforms your regulatory documents into formal ontologies with provable collision detection.