Use the same base model, training budget, and evaluation protocol for ordinary data generated by an LLM and data improved through symbolic checks and counterexamples. Report data preparation and teacher model costs separately. Include an untrained baseline and a control using prompts without training.
Back to home
Engineering method
Start with what works. Test the rest.
I use AI agents to help build systems. I decide what the system needs to do, look for methods that have worked before, and choose how to represent and check the problem. I remain responsible for deciding whether the result meets those requirements.
My research also uses neurosymbolic workflows: LLMs help me formulate questions and hypotheses, while explicit models and independent checks make those ideas testable. I guide the process and build tools to preserve its evidence.
Research method
Explore ideas, then check them.
I use LLMs to propose, predict, analyze, and recombine ideas. They help me arrive at research questions, competing hypotheses, and useful abstractions. Deterministic tools supply replayable checks of the mathematical and logical claims that emerge.
LLMs explore candidate spaces
A space is a set of possible candidates for a question. LLMs are neural models that propose, predict, analyze, and recombine candidates across many such spaces. They can transfer a useful structure between problems or suggest a new representation after a failed check.
A search can be exhaustive within a finite, declared space when every candidate is enumerated and checked. Other searches are partial or heuristic. I distinguish complete coverage from sampled exploration: both can produce valuable witnesses, counterexamples, and new questions, but their conclusions have different scopes.
- Hypothesis spaces
- Possible explanations and scientific models. Predictions and attempts at falsification help distinguish them using empirical observations.
- Witness spaces
- Candidate objects that could demonstrate a claim, such as a satisfying assignment, construction, or certificate. A verifier checks whether the proposed object satisfies the specified relation.
- Proof spaces
- Possible arguments, lemmas, and proof constructions. An LLM may propose the proof; a tool such as Lean checks the formal result under its stated assumptions.
- Design and abstraction spaces
- Alternative algorithms, representations, and decompositions. Invariant checks, equivalence checks, and experiments assess the properties that matter for the problem.
An interactive analogy
The proposer searches. The checker decides.
Imagine an LLM proposing the trajectory of a red dot through a maze. The dot leaves a red trail as the proposal is inspected. The checker establishes whether its start, moves, and destination satisfy the rules. Only an accepted trajectory turns green.
Example proposals are ready.
Enable JavaScript to animate and check a trajectory.
This demo replays recorded example proposals. A deterministic checker runs in your browser. In exploration mode, the dot marks the position currently being inspected. Animation follows your motion preferences.
A finite state space can permit exhaustive exploration, as this maze demonstrates. An unbounded maze may still have a finite solution trajectory that a checker can verify. A partial search that finds no solution does not, by itself, establish that no solution exists.
First, check the rules
An agent acts through a sequence of actions, observations, and consequences. A constitution can require every step to satisfy specified permissions and evidence requirements, including the steps before it reaches the goal.
Then compare the options
Accepted trajectories can still differ in cost, usefulness, and effects on people. In this maze, the legal detour costs more moves. In a real system, preferences and heuristics guide search among admissible options. Mathematical optimality requires a specified objective and sufficient evidence about the alternatives; a passing check alone does not establish it.
From maze trajectories to alignment
The maze walls stand for specified constraints; the goal and route costs stand for objectives and preferences. Neurosymbolic alignment combines learning better proposals with explicit checks on what a system may do. Human values determine the requirements, and the adequacy of that specification remains open to scrutiny.
- Training shapes proposals
- Use a constitution and checked examples to reward useful, permitted trajectories, honest uncertainty, and justified stopping. Counterexamples can reveal when a reward favors a shortcut through a wall.
- Monitor models raise concerns
- A learned monitor can analyze proposed actions, observed effects, and longer histories for anomalies or emerging failure patterns. Its flags can trigger a pause or review under a defined policy. Its reassurance is not a proof of safety.
- Checkers enforce specified boundaries
- Before a consequential action, check the relevant permissions, scope, and other encoded obligations. An action is accepted because those checks pass. Suggestions from another agent do not create new authority.
- Evidence improves the next iteration
- Preserve failures and their causes in Research Kernel. Revise the specification, training examples, or enforcement boundary as appropriate, then evaluate again. Measure unsafe proposals and prevented effects separately.
Monitoring and incident prevention
Prevention requires detecting a problem in time to intervene and contain its effects. OpenAI's July 2026 incident account reports earlier warning signs and monitoring improvements made with hindsight. The METR and Redwood investigation describes limitations of analysis assisted by AI. Detection, timely intervention, and effective containment each need evidence.
What a symbolic incident model adds
Represent authority, task scope, actions, and observed effects as states and transitions. A forbidden transition becomes a counterexample that can inform a regression check. Prevention still requires a faithful abstraction and enforcement over every relevant action channel: a checker cannot rule out effects its model or observations omit.
- 1. Develop the candidates
I bring the objective, domain context, and judgment. LLMs help explore explanations, alternative representations, predictions, and edge cases. I select questions that can be meaningfully tested against prior work and evidence.
- 2. Check and challenge
I choose representations and tools suited to the claim: Lean for checked proofs, Z3 for encoded constraints, Tau for formal specifications and logical reasoning, and other checkers as needed. In empirical work, I seek observations and experiments that could falsify the hypothesis.
- 3. Preserve what the evidence supports
My custom Research Kernel Protocol MCP connects hypotheses with sources, artifacts, dependencies, and refutation attempts. I preserve failures, narrow conclusions to what was checked, and use the result to guide the next investigation.
My role and my tools
Today I guide the research and judge the scope of a conclusion. Alongside Lean, Z3, and Tau, I use LEAP to investigate abstractions, my Research Kernel Protocol MCP to organize the investigation, and PopperPad to preserve hypotheses and falsification evidence.
What the checks establish
In mathematics, evidence quality comes from the proof and the checker, under stated definitions and assumptions. Solvers establish results about the constraints they receive. Research Kernel records evidence and enforces promotion requirements; the attached check or experiment supplies the substantive support.
Science: survival of the strongest hypothesis
My scientific method is inspired by Karl Popper: seek demanding attempts to falsify competing hypotheses. The hypothesis that best survives those tests earns the strongest provisional support. A useful test must be capable of exposing a failure; repeated easy tests or agreement among models add little.
Successful predictions count as evidence
A scientific model earns support when it makes a prediction and the predicted outcome is independently observed. Evidence is stronger when the prediction is specific, recorded before the outcome, and distinguishes that scientific model from plausible alternatives. LLMs help develop and analyze these models; the observations provide the empirical evidence. I weigh predictive success alongside attempts at falsification.
Support remains provisional: new evidence can overturn a conclusion, several hypotheses may remain viable, and a test may be flawed. I preserve counterevidence and unresolved alternatives so later work can challenge the result.
This public overview shows the principles, responsibilities, and evidence standards. Detailed prompts, orchestration settings, training recipes, and selection heuristics remain private.
Current research question
Can checked examples improve learned behavior?
At a fixed training budget, does training guided by symbolic checks and counterexamples improve constitutional behavior compared with ordinary training data generated by an LLM?
My Market for Behaviors essay motivates the incentive question: what behavior does a training process actually reward? My formal methods work supplies a way to express and check some of those requirements before expensive training.
The proposed loop is: specify a behavioral constitution, generate candidate examples, check the modeled obligations, use counterexamples to revise the training set, train, and evaluate on unseen scenario families. The constitution includes useful task completion alongside permissions, evidence, uncertainty, and appropriate stopping.
Track rule violations, useful task completion, unsupported claims, appropriate uncertainty, unnecessary refusals, and compute cost. Measure the learned policy's proposals separately from runtime blocking so enforcement is not mistaken for improved training. Keep evaluation labels independently reviewed and reserve unseen scenario families for the final comparison.
The initial demonstrator uses a finite behavior contract and a tabular learner to inspect reward choices. LLM assistance currently operates in the design loop. Neural weight updates and a demonstrated improvement in neural model behavior on scenarios withheld from training remain future milestones.
Constitutional AI informs feedback guided by principles; reward machines inform explicit reward structure; rewards based on rules inform feedback guided by explicit rules. These are starting points for the experiment, not evidence that this particular method succeeds.
The distinction
Think it through before you build.
Before generating code, I describe the system, its expected behavior, and the evidence I will need to accept the implementation.
I can automate much of the implementation once I have answered the basic questions: what is the system for, which rules must always hold, how should I represent them, and which independent checks will catch mistakes?
| Layer | Question |
|---|---|
| Semantics | What must this system actually do for a real user? |
| Practice | What has already been shown to work well? |
| Architecture | Which decomposition makes correctness and change manageable? |
| Verification | What independent evidence can tell right from wrong? |
| Acceptance | What evidence is sufficient for this specific claim? |
Decision loop
How I make technical decisions.
I start with methods that have worked before. If I try something new, I test whether it helps.
- 1. Understand the problem
Start with what people need the system to do and what can go wrong. For a DEX, that includes quotes, slippage, approvals, transaction status, recovery after failure, liquidity, routing, wallets, fees, and an interface that explains what is happening.
- 2. Don't reinvent the wheel
Before inventing a method, look for mature architecture, testing, UX, security, and verification practice. Ask what experienced practitioners already know, which failure modes motivated the practice, and whether it actually applies to this problem.
- 3. Choose the right abstraction
Represent the risky part in the form that makes its behavior easiest to reason about: equations for deterministic transformations, finite-state machines for lifecycle logic, invariants for safety properties, schemas for structured boundaries, or another model when it fits better.
- 4. Choose checks that fit the claim
I choose checks according to the claim, the risk of error, and the cost. These may include exhaustive enumeration, model checking, theorem proving, independent reference calculations, property tests, boundary value analysis, integration tests, or replay.
- 5. Build independent checks
Where possible, expected behavior is derived through a different path than the implementation. A spreadsheet can act as a differential oracle for deterministic financial logic; a finite-state model can expose invalid transitions; a brute-force reference can audit an optimized algorithm. Agreement is more useful when the failure modes are not perfectly correlated.
- 6. When practice is missing, run the experiment
If no reliable best practice exists, or competing practices make incompatible claims, convert the uncertainty into a comparison: define success criteria, build alternatives, construct adversarial cases, measure what works and what fails, preserve negative results, and narrow the claim to the evidence.
- 7. Keep what holds up
A successful experiment becomes a reusable local practice only after its assumptions and failure boundaries are understood. I keep what helps me make better decisions next time.
Reviewing agent-written code
Check what the code does.
For a deterministic pure core, I can write a compact description of the expected behavior and verify the implementation against it. That gives me a focused way to review code generated by agents.
For a deterministic function, I compare the implementation with an independently derived description of the expected result on the cases that matter.
domain meaning
↓
formal / behavioral model
↓
┌──────────────┬────────────────┐
│ agent-built │ independent │
│ implementation│ oracle/model │
└──────┬───────┴───────┬────────┘
└────── compare ─┘
↓
invariant checks
↓
boundary / shell tests
↓
bounded claim
Examples
Different problems deserve different workflows.
ZAL workflow
Turn a mental model into a shared formal model.
I start by describing how I think the software should behave. The LLM infers my intent and proposes semantic specifications in controlled English. I review its interpretation, correct assumptions, and test concrete examples before accepting a model.
ZAL, the Zeno Abstraction Language, gives us a shared abstract representation: my intended behavior expressed as a mathematical model that tools can work with. Controlled English, symbolic rules, and visual notation let us inspect the same declared meaning from different perspectives. The model becomes a specification against which an implementation can be checked. The goal is code that is correct by construction, with the required behavior preserved through verified refinement.
Start with the intent
“A request can reserve a resource once. Releasing it must not let the same request reserve again.”
Once this request releases the resource, it cannot reserve it again. Allowing the same request to reserve again would require a different model.
Inspect the controlled English
Three rules from the ZAL model
Rule r11: when the state is unseen and the event is reserve, if authorized, move to held.
Rule r01: when the state is held and the event is release, if authorized, move to released.
Rule r07: when the state is released and the event is reserve, if authorized, reject because duplicate and keep the state unchanged.
authorized = false is rejected; other rejection paths are omitted.I compare the English, diagram, and concrete traces with my original intent. If the LLM proposes allowing another reservation after release, I can see the changed decision and correct the model before generating code. A passing model check cannot decide whether it captured what I meant.
This example models one request identity during one process lifetime. The supplied authorization flag is an observation; authentication, persistence, concurrency, and real resource delivery need their own models and checks.
Counting constraints: controlled English and C²
A related rule can be stated as: “Every request has at most one accepted reservation.” Give each term a declared meaning, then translate the sentence:
∀x (Request(x) → ∃≤1y (Reservation(y) ∧ Accepted(y) ∧ For(y, x)))
The domain contains request and reservation records. Accepted(y) means reservation record y was accepted at some point, including if it was later released. For(y, x) associates it with request x. Counting ranges over distinct records.
This uses the two variable fragment with counting, C²: only the variable names x and y are needed, however many records exist. Zero accepted reservations satisfies “at most one”; two distinct accepted reservations for the same request violate it. Counting records alone does not specify event order or prevent repeated acceptance of the same record.
This is an illustrative C² constraint. The connected ZAL workspace's finite machine profile does not parse it; the lifecycle rules above use that separate profile. Background on C².
Full ZAL example, source, and check scope
The English below and the symbolic rules in the example model came from the connected ZAL workspace. Its lifecycle has three states, two events, and one Boolean observation: 12 declared input combinations. The displayed rules and arrows were checked against that transition table.
ZAL version 1.
The machine is one_use.
The states are held, released, unseen.
The events are release, reserve.
The context observations are authorized.
Initially the state is unseen.
Each step is atomic. Only the control state may change.
Otherwise reject because unmatched and keep the state unchanged.
Rule r00: when the state is held and the event is release, if (not authorized), reject because unauthorized and keep the state unchanged.
Rule r01: when the state is held and the event is release, if authorized, move to released.
Rule r02: when the state is held and the event is reserve, if (not authorized), reject because unauthorized and keep the state unchanged.
Rule r03: when the state is held and the event is reserve, if authorized, reject because duplicate and keep the state unchanged.
Rule r04: when the state is released and the event is release, if (not authorized), reject because unauthorized and keep the state unchanged.
Rule r05: when the state is released and the event is release, if authorized, reject because not_held and keep the state unchanged.
Rule r06: when the state is released and the event is reserve, if (not authorized), reject because unauthorized and keep the state unchanged.
Rule r07: when the state is released and the event is reserve, if authorized, reject because duplicate and keep the state unchanged.
Rule r08: when the state is unseen and the event is release, if (not authorized), reject because unauthorized and keep the state unchanged.
Rule r09: when the state is unseen and the event is release, if authorized, reject because not_held and keep the state unchanged.
Rule r10: when the state is unseen and the event is reserve, if (not authorized), reject because unauthorized and keep the state unchanged.
Rule r11: when the state is unseen and the event is reserve, if authorized, move to held.The versioned ZAL grammar defines this controlled English. Its fixed vocabulary and syntax give these sentences precise meaning. I review the LLM's proposed specification to check that it matches my intent.
What establishes correctness?
The formal connection is refinement: under the declared assumptions, every observable behavior of the implementation is allowed by the behavioral model. The controlled English and the model must have the same formal meaning, and the model must satisfy the formalized requirements. My review checks that those requirements capture what I intended.
One precise statement of that alignment is:
α(BehA(P)) ⊆ BehA(M) = ⟦E⟧A ⊆ RA
Here P is the program, M the model, E the controlled English, and A the assumptions. Beh denotes all complete observable executions; α maps implementation observations to the model's vocabulary; RA is the set of executions satisfying the formal requirements under those assumptions. The chain establishes that the implementation satisfies those requirements. Requirements about completion add termination or progress obligations.
When synthesis or generation establishes these relations through checked refinement proofs as it constructs the implementation, the result is correct by construction with respect to the specification and assumptions. This is the approach illustrated by proof-producing program refinement. An independent proof can also establish correctness of code after it has been generated. For a finite system, exhaustive refinement checking can establish the relation across its complete declared domain.
A claim about a deployed build must explain how the proof reaches that executable, including the stated trust assumptions for compilation, the runtime, and the environment. Semantic preservation in verified compilation provides one formal link in that chain.
Evidence for this example: the completed check covers the 12 declared input combinations of the reservation model and the displayed rules and arrows. ZAL's refinement guide describes the additional comparison between a model and a generated application's behavior. That implementation comparison was not run for this page's example. The C² example remains a separate explanatory constraint.
Functional core, imperative shell
Put deterministic state evolution in a pure core where behavior can be exhaustively tested, modeled, or proved. Keep external effects in a narrow shell and cover that boundary with integration, replay, idempotency, and failure tests.
Finite-state review
Model the possible states and the transitions between them. Check which transitions are allowed, which are missing, and which should be impossible.
Differential financial audit
Write the expected equations independently in a spreadsheet or reference model. Compare its results with the implementation using inputs that could reveal a disagreement.
Boundary value analysis
Test empty and full states, minimums and maximums, and values just below or above a limit. Small changes at these points can reveal mistakes.
Arrange, Act, Assert
Set up the starting conditions, perform an action, and check the expected result. Each test should make clear which behavior it checks.
When there is no best practice
Define success, compare the approaches on a stated problem, and record the failures and successes. Keep the approach that holds up, along with the conditions under which it worked.
Best practice as a hypothesis
Good practice should stand up to testing.
I ask what makes a practice worth following: which problems has it prevented, under what conditions, and at what cost? When those conditions change, I test it again.
I also learn from what goes wrong. Recording how an approach failed helps me avoid repeating the same mistake.
Use mature practice when its assumptions match the problem.
Modify practice when the environment changes, while preserving the reason it existed.
Turn competing recommendations into a bounded empirical or formal comparison.
Experiment, preserve failures, and promote only what the evidence supports.
Human + agents
I remain responsible for the tasks I delegate.
Agents help me research, build, refactor, generate test cases, and explore possible designs. I record what I asked them to do, which methods and models I chose, how I checked the results, and what I personally reviewed.
I disclose how AI was used and explain why I accepted the result. The design and the checks matter as much as the code.
Architecture is choosing the right abstraction and the right evidence before the code exists.
Operating method
Evidence
Put the method to the test.
The Capabilities page connects these ideas to work samples. The evaluation section within Value brings together sources, verification commands, and the limits of the evidence.