Skip to main content
Refactron is the deterministic gate LLM agents call before they land a change. The agent proposes; Refactron proves. That division of labor is the whole design.
A probabilistic model proposing a change, handed to Refactron's deterministic verifier, which returns the same reproducible verdict every time

A probabilistic proposer, a deterministic verifier: the same repo state and diff always produce the same verdict.

​
Two different jobs

Writing code and certifying that a change is safe are different problems, and they want different tools.
  • Generating a change is a good fit for a probabilistic model. An LLM explores a huge space of plausible edits and usually lands on a reasonable one. Different runs can produce different code, and that’s fine; you’re going to check it.
  • Deciding whether that change preserved behavior is a formal problem. The answer must be reproducible: the same repo state and the same diff have to yield the same verdict, every time. A judgment you can’t reproduce isn’t proof; it’s another opinion.
Put a probabilistic proposer behind a deterministic verifier and you get the best of both: fast generation, and an answer you can stand behind.

​
What “deterministic” buys you

Refactron’s verification engine (the shadow tree, the three gates, and the coverage check) contains no model, no temperature, no sampling. Run a verify twice on the same inputs and you get the identical verdict and the identical report. That reproducibility is what makes the verdict usable:
  • An agent can act on it. A SAFE / UNSAFE / UNPROVEN answer that flips between runs is worthless as a gate. A stable one is a decision an agent, or a CI job, can branch on.
  • A human can audit it. “The tests passed and these exact lines ran” is a claim you can re-check. “The model thought it looked fine” is not.
  • It stays honest. When the evidence isn’t there, a deterministic gate returns UNPROVEN instead of guessing. It never rounds “I’m not sure” up to “looks good.”

​
Where a model does fit

The verdict is never a model’s call, and as of 0.4.0 there is no model anywhere in Refactron. Earlier versions shipped an optional document command that generated docstrings and changelog prose on top of an already-verified diff; it was removed with migration mode. Even then the rule held: a model was welcome where fluent language was the goal, and kept out of the path that decides whether a change is safe. That’s the rule the whole product follows: models are welcome where fluent language is the goal, and kept out of the path that decides whether your change is safe.

​
The takeaway

You don’t have to trust Refactron the way you trust a model. You can re-run it and get the same answer, read exactly which gates passed and which lines your tests exercised, and see the reasoning behind every verdict. Determinism isn’t a limitation here; it’s the feature that lets an agent hand off the one job it’s worst at.

​
Citations

The idea that a transformation is only safe once explicit preconditions hold (the conceptual root of a deterministic gate) comes from Bill Opdyke’s 1992 thesis.
  • Opdyke, William F. Refactoring Object-Oriented Frameworks. PhD thesis, UIUC, 1992. PDF