Guess Close, Search Exact: A Formally Verified, Model-Free Memory and Mutation Engine for Language-Model Agents

Language models are good at proposing roughly right answers and poor at being exactly right, cheaply, every time. neo4d is a model-free engine that sits beside a model: it mutates code token by token and lets the tests judge every variant, searches the neighbourhood of a model's attempt, and remembers verified work as placeholder plans it can replay without the model. What it trusts is decided by RELATE v2, an eight-bit integer law with no branches, checked on all 2^32 inputs for undefined behaviour (UBSan, CBMC); its nine principles hold on every reachable input and eight further properties on all 256 eight-bit inputs. Under a teacher that gives 10% wrong lessons, the law keeps 58.4% of what memory produces correct, against 0.9% when every pattern is trusted at first sight and 1.7% without its barren rule, at equal coverage. With neo4d, phi4-mini fixes 62.5% of 176 bugs (30.7% alone, 42.0% with three tries) and completes 47.1% of 85 multi-step agent tasks (25.9% alone, 40.0% with three tries) with fewer calls. Claude Sonnet and Claude Haiku keep their accuracy (85/85, 84/85) while neo4d takes 32% and 40% of the tasks off them; a replayed plan takes 0.59 s against 20-36 s for a model. With Haiku only choosing which branches to explore, neo4d's search fixes 17 hard two-fault bugs where a blind search fixes 14 and a random filter 12.0, with 60% fewer test runs. On real bugs at an equal budget over three seeds, a loop in which neo4d mutates each of the model's attempts fixes 24.7 of 31 with gemma3:4b against 16.0-18.7 for sample-and-filter, self-debugging and Reflexion (p <= 0.016) with about 35% fewer calls; with phi4-mini it leads (23.0 against 20.0-22.3) without a significant difference. On two domains that are not code - a numbers puzzle and block-stacking plans - the same core, unchanged, lifts both small models far above their own methods (Countdown: from 0 to 26-31 of 40), but its search alone, with no model, does as well or better: there the small models' guesses are worse starts than a neutral one. Negative results are reported equally: evidence handed to a small model as a paragraph made it worse, marks on suspect lines helped one model and hurt another, and nothing helped on bugs a strong model already solves. Implementation, experiments and text were produced with Claude Code (Anthropic) under the author's direction. Code, results and every run: https://github.com/devkancheti4-design/neo4d. SWE-bench results will follow in a later version.