From Aristotle to Runtime: Formally Provable TypeScript and AI That Verifies Its Own Code

Large language models can generate code that looks perfectly convincing even when it does not work. We respond by writing larger prompts, expanding the context window, and adding RAG — yet the model may still produce a program that confidently explains its own failure. But what if the real problem is not generation quality? What if the model simply has no reliable way to verify its result as an engineer would?

In this talk, we will follow a conceptual path from Aristotle’s syllogisms and enthymemes through Boolean algebra, sets, groups, and category theory. We will explore how these seemingly academic ideas can become a practical language for describing programs in terms of objects, transformations, composition, and functors.

I will introduce a TypeScript superset of my own design. In a single file, a developer describes a utility through its category, object types, valid transformations, relationships, and functors. This specification constrains the solution space available to AI and allows it to generate code that is not merely syntactically plausible, but formally provable against explicitly defined properties.

Along the way, we will encounter Church encodings, immutable data structures, logical paradoxes, and the troublesome idea of a universal set. We will also see how functional programming reduces the number of possible program states and gives both humans and AI fewer opportunities to make mistakes.

Formal constraints, however, are only one half of the solution. In the second part of the talk, I will present the architecture of a custom runtime self-verification system.

The AI first generates a draft rather than a final answer. A separate binary instruments the generated program, wrapping executable expressions and collecting their signatures, runtime types, values, state transitions, branches, and errors. The draft is then executed in an isolated environment. Its execution trace is returned to the model, allowing the AI to diagnose and fix its own code before the result reaches the user.

We will examine how generation, instrumentation, execution, evaluation, and correction form a repeatable engineering feedback loop. We will also discuss isolation, timeouts, resource limits, side effects, trace compression, and the conditions under which the agent should stop trying to repair a solution.

I will then connect this architecture to the scientific method and advanced prompting techniques, including zero-shot and few-shot prompting, RCTF, ReAct, Tree of Thoughts, RAG, and STAR. The goal is not to collect more prompting acronyms, but to move from “ask the model to write some code” to a disciplined cycle of hypothesis, experiment, observation, and correction.

Finally, I will share how I tested these approaches at Avito: which scenarios I selected, which baselines I compared, and how I measured correctness, retries, regressions, token usage, latency, cost, and human intervention. We will also look at the cases where automated verification genuinely improves the result — and those where it merely produces a more expensive hallucination.

After the talk, attendees will leave with:

• an architecture for building AI coding systems with runtime feedback;
• a model for adding formal specifications to TypeScript programs;
• a practical framework for evaluating AI-generated code without relying on confidence, eloquence, or prompt magic.