I build AI that manufactures its own products — and puts every claim through a theorem prover before it ships.
The proof isn't an argument. It's a factory that has been running unattended for six days, and everything it made is public.
🌑🏭 dark-factory-live — running right now
Every six hours, with no human in the loop, it picks a subject and researches it. Nothing enters the result until the knowledge is proven coherent. What comes out is installable software, published as its own public repository and rendered to a live site.
| 8 | public knowledge products shipped, in 6 days |
| 4,426 | machine-grown concepts, every one admitted by a theorem prover |
| 92 → 11 | pull requests it opened against its own source. It merged 11 and rejected 81 |
See it: KB Atlas (a live graph page per module) · the marketplace · restaurants-module (2,849 concepts) · the clean source line
Every concept and relation is admitted through a SWI-Prolog consistency gate that proves the graph is closed (no relation points at an undefined concept) and connected (no orphans). When it isn't, the prover names exactly what's missing — and that becomes the next unit of work. Each finished module ships four ways: as RAG, as an agent you can ask, as tools, and as OWL/Turtle — a real machine-readable ontology.
The honesty is the flex: the gate proves coherence, not truth. Factual wrongness is expected. It gets priced by how far it spreads and worked off through open supersede issues, never silently retracted. No slop generator can print that sentence.
The same factory turns on its own source. AI agents convene inside a game and work out what the repo needs. Three gates then decide, each killing a different failure mode:
| gate | what it kills |
|---|---|
| The market — a peer agent has to pay for the idea | self-assessed value |
| The fresh-model test — a blank AI instance must follow the procedure from its text alone, and the system mints the test record itself | work that only functions with its author in the room, and forged records |
| The replicated race — the patched version must out-produce a control, same conditions, repeated | changes that are plausible and well-argued but useless |
It opens a real pull request either way. Merged PRs are proven improvements; closed PRs are the graveyard of ideas that didn't survive measurement. Both are public, and the rejections outnumber the merges eight to one.
The design bet, in one line: you don't need the proposer to be right — you need the selection structure to be sound.
| ee-v2 · MIT | The engine that powers the knowledge line — the curried compiler, the language automaton, the brain, the OWL projection. |
| carton-mcp · PyPI | A knowledge-graph platform for agent memory — 38 tools, retrieval state machines stored as graph data, shipped as an authenticated service with quota metering. |
| cave-teams · PyPI | Compose AI agents into teams and topologies, with routing and gates, plus a library of proven teams. |
| chaincompiler | A fully customizable prompt-engineering language and agent compiler: deterministic, versioned, testable prompts instead of ad-hoc strings. |
| skilltree · PyPI | Coordinate-addressed skill systems, so an agent loads the right capability at the right moment instead of drowning in a flat library. |
| heaven-framework · PyPI | The agent framework underneath it all — what an agent is: configs, chains, tools, memory. |
| owl22python · PyPI | Bidirectional OWL2 ⇄ Python. Every class knows its own ontology. |
Philosophy → screenwriting → ontologies → and then LLMs came out.
I was building ontologies before there was anything to run them on. Philosophy taught the discipline — what makes a thing the thing it is. Screenwriting was applied ontology under deadline: beat sheets, character matrices, story grammars, structure that either holds or the script dies.
Then LLMs arrived and I climbed the ladder everyone climbed — prompts → personas → cognitive prompts → tools → agents → agentic apps as tools — and at the top I hit the wall everyone hits: oh wait, I need logic.
The field went around it. Embeddings, RAG, bigger context, more prompt. I went down, because I already had the thing that was missing. Logic engines → ontology agents → and then the rung that's on nobody's ladder: ontologies that do the cognition for the agent. Not a store the agent queries. The ontology reasons; the agent acts on what it concluded.
Only afterward did I recognize where I'd arrived — this is the system the semantic-web program specified in 1999 and never got: machine-readable ontologies that agents traverse, reason over, and act on. It runs at 3.5 million terms, where the standard tooling costs two minutes on a few hundred.
That's not a thesis anymore. It's the eight modules above — each one a formal ontology, prover-admitted, shipped as software, with an agent attached that reasons over it.
Three years. Solo. From zero prior code.
📫 isaacwrubin@gmail.com · 🌐 sancovp.github.io/aisaac · 📄 ORCID 0009-0003-0219-0506
Available for consulting and full-time roles — agent architecture, MCP integration, and making autonomous AI safe to ship.