Alexander Feldman's Blog

Category: Research

  • Cranks of the First and Second Kind

    Draft. Thinking aloud. This is the beginning of a research statement, not the end of one.

    This morning, Nvidia committed five billion dollars to Safe Superintelligence, the company founded by Ilya Sutskever, in exchange for equity and a promise to multiply its compute tenfold within a year. SSI has, to date, shipped no product, published no research, and demonstrated no commercial traction. This is not a criticism of SSI — it is simply what the reporting says. Five billion dollars and a tenfold increase in compute for a company whose founder went on record last year to say that the age of scaling is ending. One admires the internal consistency of an industry that responds to “more compute will not be enough” by purchasing more compute. Nvidia’s own stock closed down about five percent on the day, which suggests the market has at least a rudimentary sense of irony even when the participants do not.

    Meanwhile Meta is spending seventeen billion dollars a quarter on capital expenditure and promising “personal superintelligence for everyone,” a phrase that has the same relationship to engineering that “subterranean opportunity space” has to a hole in the ground.

    Let us talk about cranks.

    A Taxonomy

    When I was younger and read physics for pleasure, there was a reliable genre of correspondence: the letter, usually typed, usually with underlining, announcing the discovery of a perpetual motion machine. The pleasure was not in the discovery — there was never a discovery — but in the classification. You read the argument, you found the error, and you filed the author.

    A crank of the first kind claims a machine that produces energy from nothing. He violates the first law of thermodynamics: conservation of energy. His diagram has a wheel with weights on it, and if you follow the weights around, they do not come back to where they started.

    A crank of the second kind is more sophisticated. He concedes conservation of energy. He does not claim to make energy; he claims only to extract it — from the ocean, from the ambient air, from the vast reservoir of heat that surrounds us and is admittedly free. He violates the second law. He has invented a machine that takes disorder and returns order, at no cost, and he has not noticed.

    The second kind is always the more interesting letter, because the error is deeper and the author is usually cleverer.

    I propose that the same taxonomy applies, exactly and usefully, to claims about computation. And I propose it in a spirit of genuine intellectual charity, because the classification is not an insult. It is a diagnostic procedure, and I have spent twenty years building diagnostic procedures.

    A crank of the first kind in computer science claims to solve NP-hard problems in polynomial time. He violates P ≠ NP. This is technically a conjecture rather than a law, but it is the best-supported conjecture in the subject, and if you propose to overturn it you had better bring a proof rather than a benchmark. These letters still arrive. They are honest, at least, about what they claim.

    A crank of the second kind concedes the complexity classes entirely. He agrees that travelling salesman is NP-hard, that circuit minimisation sits at the second level of the polynomial hierarchy, that model counting is #P-complete. He agrees to all of it, cheerfully, and then explains that his system does not need to solve the worst case, because it has learned the structure of real instances. It has absorbed, from a corpus, the shape of the answer. It will simply produce the correct output without searching for it.

    This is the machine that extracts work from a single heat bath. He has proposed to obtain a certificate — a guarantee, a proof, a thing you can check — from a process that produces no certificate, and he has not noticed the difference between an answer and an answer you can verify. He has confused a plausible output with a sound one. The energy is free, the ocean is vast, and the machine will run forever.

    There is now a third kind, unknown to classical thermodynamics, who does not claim to solve anything at all and raises five billion dollars regardless. He violates no law of physics. He violates only the conservation of shareholder value, and that quantity was never conserved to begin with.

    I will spend the rest of this post explaining why I believe the second-kind classification is correct, and what I intend to do about it, which is the actual purpose of the exercise.

    Where I Have Been

    Nowhere intellectual. I travelled, I did summer things, I saw people, I did not write. The blog went quiet after Delft and the Cerebras IPO and the AI café ordering eggs for a kitchen with no stove. I recommend the pause. Things settle.

    I am back, and I am back with a specific problem: I am defining projects, looking for gigs, and — most importantly — returning to research. Returning to research requires knowing what your research is, which requires writing it down, which is what this is. Consider it a first draft with the seams showing.

    The Universe Is an Optimisation Problem

    Start where physics starts. The principle of least action says that a system evolving from one configuration to another takes the path that makes the action stationary. Fermat’s principle says light takes the path of least time. Soap films find minimal surfaces. The Euler–Lagrange equations are what you get when you set a derivative to zero and solve.

    This is not a metaphor. The universe really does compute, and what it computes is the stationary point of a functional. Newtonian mechanics, electromagnetism, general relativity, the Standard Model — all of it can be written as “here is a Lagrangian, now find where the variation vanishes.” The universe is a very large, very fast, very well-conditioned optimiser, and the method it uses is the derivative.

    Which is to say: the universe does gradient descent.

    And this is precisely the point at which the argument turns, because the second observation follows immediately from the first:

    The universe does gradient descent, and therefore the universe does not solve NP-hard problems either.

    The evidence is everywhere, and it is embarrassing:

    • Soap films do not solve Steiner tree. The folklore claim — dip a frame in soapy water, get the optimal network — is false, and it has been tested rather than argued about. Films get stuck in local minima. They find a minimal surface, not the minimal surface, and which one depends on how you pulled the frame out of the bucket.
    • Proteins misfold. Levinthal’s paradox observes that a protein cannot be searching its conformation space, because the search would outlast the universe, and yet folding happens in microseconds. The resolution is that nature is not searching — it is rolling downhill on a funnel-shaped landscape. It works most of the time. When it does not work you get amyloid plaques and prions, which are what a local minimum looks like from the inside.
    • Spin glasses do not find their ground state. Determining the ground state of a three-dimensional Ising spin glass is NP-hard. A real piece of spin glass, cooled in a real refrigerator, does not find it. It ages, it hystereses, it gets stuck, and it stays stuck for geological time.

    The universe is a superb gradient descender and a hopeless combinatorial optimiser, and these are the same fact stated twice. This is why the “analog computer solves NP-complete problems” genre is a permanent fixture of the crank literature: it is the exact physical analogue of the perpetual motion machine, and it fails for a reason of the same character.

    Integers Are Where It Gets Hard

    I have spent an unreasonable fraction of my professional life on this, so permit me some specificity.

    Gradient descent needs three things: a continuous domain, a differentiable objective, and a landscape on which local information is informative. Given those, it is magnificent. Modern deep learning works not because anyone found a clever algorithm but because, in sufficiently high dimension and with sufficient overparameterisation, the loss landscape turns out to be benign — mostly saddle points rather than bad local minima, mostly connected basins. You take the derivative, you step, you repeat, and it works. Nobody fully knows why it works this well. It works.

    Now require the variables to be integers.

    Every one of the three things breaks at once. The domain is the vertices of a hypercube; there is no gradient on a vertex. The objective is defined only at those vertices; there is nothing to differentiate. And local information stops being informative — flipping one bit can move you anywhere.

    The standard rescue is relaxation: let your binary variables live in [0,1], solve the resulting continuous problem, and hope. This is the foundation of half of operations research and it is genuinely powerful. But notice what it gives you. It gives you a bound, not an answer. The distance between the relaxed optimum and the true integer optimum is the integrality gap, and closing it is the entire discipline: branch and bound, cutting planes, Lagrangian relaxation, column generation, symmetry breaking, forty years of the Mixed Integer Programming literature. The relaxation tells you where the answer cannot be. Finding where it is requires search.

    Nor can you simply round and call it a day. For a large class of problems, no polynomial-time procedure can get you close. Håstad’s result on MAX-3SAT says that beating a 7/8 approximation is itself NP-hard. This is not “we have not found the algorithm yet.” This is a theorem about what rounding can do.

    And where does the guarantee come from, when you have one? From duality and from exhaustion. LP duality gives you a certificate: a dual feasible solution that proves no better primal solution exists. Branch and bound gives you a certificate: a search tree, every branch of which was closed by a bound or a proof of infeasibility. A SAT solver that reports UNSAT can hand you a resolution refutation and you can check it independently with a program you wrote yourself in an afternoon.

    A gradient step produces no certificate. It cannot. It is a local move on a continuous surface, and its output is a slightly better point, not a proof about all other points. Ask it for a proof and it has nothing to give you, because proofs are not the kind of object it manufactures.

    Which Brings Us to the Chatbots

    The training objective of a large language model is cross-entropy on next-token prediction. Gradient descent descends that. There is no theorem — not a weak one, not a conditional one, not one anybody has attempted — connecting low cross-entropy loss to correctness of a mathematical argument. The loss went down. That is what has been established.

    There is also a structural point that deserves more attention than it gets. A transformer forward pass is a fixed-depth circuit. Fixed-depth, polynomial-size, threshold-gated circuits are the class TC0, and TC0 does not contain NP-hard problems unless a great deal of complexity theory is wrong. Each token costs a bounded amount of computation, and no amount of parameter count changes the depth.

    The escape hatch is chain of thought: use the context window as a tape and you recover, in principle, a general computation. Fine — but now you are running a Turing machine on a substrate with no error detection and no error correction, and every step is sampled rather than derived. This is not an incidental defect to be engineered away. Hallucination is what an unverified tape looks like. It is the same phenomenon as a soap film in a local minimum: the process ran, it terminated, it produced something, and nothing in the process was ever obliged to produce the right thing.

    So: chatbots will not do theorem proving. And here I want to be precise, because the imprecise version of this claim is itself crankery, and I would rather not be classified by my own taxonomy.

    What is actually happening in the Lean ecosystem right now is that language models propose and kernel checks. Models generate candidate formalisations and candidate tactic scripts; a small, auditable, deterministic proof kernel accepts or rejects them. Some real results have come out of this, including formalisations of things that were open. This is genuine and I have no interest in denying it.

    But look at where the guarantee lives. It lives in the kernel. It lives in a few thousand lines of code that implement a type theory and can be read by a human being in a week. The model is a proposal distribution — an extremely expensive, occasionally brilliant heuristic for generating candidates. It is playing the role that a branching heuristic plays inside a SAT solver: it makes the search faster and it makes no promises. Take the kernel away and you have a machine that emits confident LaTeX.

    The gradient proposes. The verifier disposes. Anyone who tells you the gradient is doing the proving has confused the two, and the confusion is exactly the second-kind error: mistaking a plausible output for a sound one, and expecting a certificate from a process that emits none.

    So What Am I Actually Doing

    Here is the research statement, in draft.

    The interesting problems live at the boundary between the continuous and the discrete, and almost nobody works there. The continuous side is well served — that is physics, that is simulation, that is the entire deep learning industry. The discrete side is well served by the SAT, SMT, QBF, and MIP communities, who are serious people doing serious work with certificates. The boundary is thinly populated and it is where the real systems are.

    My own work has been sitting on that boundary for twenty years without my having named it properly:

    • Model-based diagnosis is exactly this shape. The fault hypotheses are discrete — this component is healthy or it is not, and there are 2n of them. The behaviour is continuous — ODEs, DAEs, SPICE models, thermal gradients, feedback. Lydia-NG exists because Boolean models are wonderful for switching circuits and useless for anything physical. A hybrid diagnostic engine is a mixed-integer problem wearing a lab coat.
    • Exact synthesis — qbf-designer — is Σ2p-complete and gets exact answers where Vivado and Yosys get heuristic ones. Five LUTs where the heuristic finds six. The point is not that five is smaller than six. The point is that I can prove there is no four.
    • Diagnostic probability is a counting problem, and counting is harder than deciding. The posterior of a diagnosis is a ratio of model counts: how many assignments of the internal signals are consistent with the model, the observation, and this fault hypothesis, over the total. That is #P-complete. LyDiA got this wrong for a decade — it multiplied independent priors together and called the product a probability — and the modern llogic packages fix it. What I still cannot resolve is that every diagnostic probability is therefore a rational, a ratio of two integers, and physical failure rates are not obviously rationals at all. That one keeps me up.
    • Technology mapping for Verilog and VHDL is where I think the near-term commercial value is, and my Delft friends have graciously confirmed it is not entirely a hallucination.

    And the part I need to think harder about: where the learned heuristics legitimately belong. They belong inside the sound framework, not instead of it. Branching order. Variable selection. Restart policy. Which cut to add. Candidate proposal for a kernel to check. All of these are places where a model that is right 70% of the time makes a sound solver dramatically faster and never makes it wrong, because the soundness was never the model’s job. That is a research programme I can defend to a referee, and it is roughly the opposite of the one currently being funded at five billion dollars a pop.

    The universe does gradient descent, and it is very good at it, and it cannot factor a number. The industry has built a magnificent gradient descender and is now surprised that it cannot factor a number either.

    More soon, and with code. As always, everything I discuss is reproducible, which continues to distinguish it from most of what is published within a fifty-mile radius of here.

    Ceterum censeo slopem esse delendam.

    (Cato the Elder ended every speech in the Roman Senate with “Carthage must be destroyed” — regardless of the topic. This is that, but for AI slop.)

  • AI-Generated Spaghetti Slop Considered Harmful

    The Balkanization of AI is happening: Google fights OpenAI fights Microsoft fights Meta, while I am pondering on how early I should go to Oakland’s court to get free entertainment from seeing the Musk vs Altman trial. Why this is going to entertain me is probably analogized by the shrinks with the phenomenon of why relatively educated people in Europe listen to turbo folk music. Good that the court system does not (still) allow avatars as Zuckerberg throws considerable amount of energy into building his own AI duplicate.

    In the background of all this, I am quietly growing my circuit analysis and synthesis framework. Last week I wrote about DSLs and their advantages. Today I decided to implement the parser. It took me half an hour, and this is the lark grammar:

    start: (import|module)+

import: IMPORT ESCAPED_STRING

module: MODULE CNAME "(" ports ")" ":" (gate | wires | instantiation)* END

ports: port (";" port)*

port: (INPUT | OUTPUT) CNAME array? ("," CNAME array?)*

gate: CNAME ":" CNAME "=" CNAME "(" CNAME ("," CNAME)* ")"

wires: CNAME ("," CNAME)*

instantiation: INST CNAME CNAME "(" assignment ("," assignment)* ")"

assignment: CNAME array? "=" CNAME array?

array: "[" INT (":" INT)? "]"

IMPORT: "import"
MODULE: "module"
END: "end"
INPUT: "input"
OUTPUT: "output"
INST: "inst"

%import common.INT
%import common.CNAME
%import common.ESCAPED_STRING
%import common.WS
%import common.SH_COMMENT

%ignore WS
%ignore SH_COMMENT

    Just out of curiosity, I wanted to see how bad the slop generator is, and ChatGPT did not fail to disappoint. I will not put here the generated grammar as I want to preserve the reader’s sanity, but it is ugly and 71% longer. It also generated an Abstract Syntax Tree that is 36% bigger. If I was a research assistant in compiler construction, such a homework would immediately get grade five (in The Netherlands, where I studiedwent to university) grades are from one to ten, one to five are all failing grades, I suppose it is good to know that you almost made the exam).

    Of course, this grammar produces an Abstract Syntax Tree that has too much detail for good analysis. Luckily, Lark provides AST transformation classes which promise to be tidy and neat and different from slop. That is what is going to be my next GitLab push.

    Ceterum censeo slopem esse delendam.

    (Cato the Elder ended every speech in the Roman Senate with “Carthage must be destroyed” — regardless of the topic. This is that, but for AI slop.)

  • Teaching a Language to Think in Hierarchies

    Bitcoin miners are liquidating their holdings to pivot into AI hosting. The machines that wasted electricity producing imaginary money will now waste it producing imaginary intelligence. Anthropic has secured 3.5 gigawatts of compute — the consumption of three and a half million households — to serve language models.

    GCC compiles the entire Linux kernel in fifteen minutes on a single machine drawing 200 watts. Fifty watt-hours. A light bulb left on for an afternoon. It manages this because it is not guessing. It has a grammar, a type system, and an optimisation pipeline where every transformation preserves semantics. There is no temperature parameter. There is no “try again and hope.”

    A compiler’s cost is \(O(n \log n)\) in the size of the input. A language model’s cost is \(O(n \cdot d)\) where \(d\) is the dimensionality of a model that cannot tell you whether the answer is correct. When the task has a formal specification, you do not need gigawatts. You need a parser.

    I have been writing parsers for twenty years. Today I started improving the one that matters most: the circuit description language at the heart of llogic, qbf-designer, and the formal methods toolchain I am building at Llama Logic.

    My first encounter with a compiler was at Zend Technologies in Ramat Gan in 2000. I was twenty-two, fresh off the plane from Bulgaria, and I did not know what a parser was. Zend built the PHP language engine. I watched a small team turn a grammar into a working language that ran half the web. I did not understand how.

    A few years later, at Delft, I read the Dragon Book and took the compiler construction course of Koen Langendoen. We became friends over my many years at the university. That course turned out to be one of the most useful things I have ever learned. It is the skill that lets me write software that works — not approximately, not statistically, not when the vibes are right, but deterministically, on all inputs, by construction.

    It is also how I got into diagnosis. At the end of my master’s I went to Koen and asked for a Ph.D. position in compiler construction. He told me “compilers are passé” — but I could go work with Arjan J.C. van Gemund doing diagnostics. Arjan has since retired north to compose music, which is a better use of a fine mind than supervising Ph.D. students, though he was good at both. They needed a compiler for LyDiA, the diagnostic modelling language. So I built one. Then I built many more. Every research system I have worked on since — LyDiA, the DXC framework at NASA Ames, the synthesis tools at PARC, and now llogic — has a parser at its core. The compiler is never the point. The compiler is always the point.

    A domain-specific language is a small language built for one job. SQL is a DSL for databases. Regular expressions are a DSL for pattern matching. Makefiles are a DSL for build dependencies. You do not write an operating system in SQL. You do not query a database with a Makefile. The language fits the problem, and because it fits, it can enforce constraints that a general-purpose language cannot.

    This is the point that the vibe-coding movement misses entirely. A grammar is not a convenience. It is a contract. When I write a parser for a circuit description language, the grammar specifies exactly what constitutes a valid circuit. If you misspell a gate type, the parser rejects your input. If you connect an output to a nonexistent signal, the parser tells you. If you instantiate a module that does not exist, you get an error message with a line number — not a plausible-looking circuit that silently computes the wrong function.

    This is what determinism means in practice. The parser either accepts or rejects. There is no 95% confidence. There is no temperature. The same input produces the same result every time, on every machine, for every user. A QBF solver receiving a malformed netlist will produce garbage. A diagnosis engine receiving an inconsistent model will compute meaningless results. The parser is the gate that keeps garbage out. It costs milliwatts. It works.

    There is a second reason, less often discussed. Humans need to read these things. An engineer debugging a faulty adder needs to look at the circuit description and understand it. A reviewer verifying a synthesis result needs to confirm that the specification matches the intent. This is not a machine-to-machine format. It is a language — with the same design obligations as any language: clarity, consistency, and the ability to say exactly what you mean and nothing else.

    The circuit DSL in llogic had outgrown its grammar. The new format adds modules, arrays, imports, and arbitrary nesting. A full adder, from primitives to a 4-bit module with array slicing:

    # 4-bit ripple carry adder

import "std_logic.circ"

module half_adder(input a, b; output s, c):
    x: s = xor(a, b)
    a: c = and(a, b)
end

module full_adder(input a, b, ci; output s, co):
    wire f, p, q

    inst half_adder ha1(a=a, b=b, s=f, c=p)
    inst half_adder ha2(a=ci, b=f, s=s, c=q)
    o: co = or(p, q)
end

module adder2(input a[2], b[2], ci; output s[2], co):
    wire c0

    inst full_adder bit0(a=a[0], b=b[0], ci=ci, s=s[0], co=c0)
    inst full_adder bit1(a=a[1], b=b[1], ci=c0, s=s[1], co=co)
end

module adder4(input a[4], b[4], ci; output s[4], co):
    wire cm

    inst adder2 lo(a=a[0:1], b=b[0:1], ci=ci, s=s[0:1], co=cm)
    inst adder2 hi(a=a[2:3], b=b[2:3], ci=cm, s=s[2:3], co=co)
end

    Four levels of nesting. Modules, arrays, slices, named connections. The flattener — a recursive tree walk, the same algorithm I used in LyDiA for system descriptions — traverses the instantiation tree and emits the flat netlist the solver has always consumed. The hierarchy is for the engineer. The solver does not know it exists.

    Sequential circuits work the same way. A 4-bit serial adder with synchronous reset:

    # 4-bit serial adder with synchronous reset

module shift4(input d, rst; output q):
    wire d1, d2, d3

    f1: d1 = dff(d, rst)
    f2: d2 = dff(d1, rst)
    f3: d3 = dff(d2, rst)
    f4: q = dff(d3, rst)
end

module seq_adder4(input a, b, rst; output s, co):
    wire i1, i2, ci

    inst shift4 sa(d=a, rst=rst, q=i1)
    inst shift4 sb(d=b, rst=rst, q=i2)
    inst full_adder fa(a=i1, b=i2, ci=ci, s=s, co=co)
    c: ci = dff(co, rst)
end

    A dff with one argument is a plain register. Two arguments: synchronous reset. This maps directly to the standard Verilog template always @(posedge clk) if (rst) q <= 0; else q <= d; — making translation between the two languages mechanical.

    So why not just use Verilog?

    Because Verilog is a simulation language that has been coerced into serving as a synthesis input. A synthesis tool reads an always block, pattern-matches the sensitivity list, and infers what is a register and what is combinational logic. The engineer writes behaviour and hopes the tool’s heuristics match their intent. In llogic, a dff is a dff. An and is an and. There is no inference. The circuit says what it is.

    This matters for formal methods. Diagnosis requires knowing exactly what components exist. Synthesis requires a precise specification of the design space. Neither tolerates a language that hides structure behind inference rules. Verilog is the right language for RTL designers who want to describe behaviour and let tools figure out the structure. Llogic is the right language when the structure is the point.

    The parser, AST, and flattener should take a few days. When they are done I will update the llogic repository on the feature/hierarchical-dsl branch.

    Three and a half million households’ worth of electricity to serve a model that cannot tell whether it is thinking deeply or not. Fifty watt-hours to compile a kernel. Considerably less to parse a circuit. The tools that work have always been quiet, small, and correct. The software will continue to not hallucinate.

    Ceterum censeo slopem esse delendam.

    (Cato the Elder ended every speech in the Roman Senate with “Carthage must be destroyed” — regardless of the topic. This is that, but for AI slop.)

    Repository: llogic

  • What’s Actually Broken

    Amazon’s weekly operations meeting in March reportedly focused on a “trend of incidents” characterised by “high blast radius” and “Gen-AI assisted changes.” The Financial Times, which saw the briefing note, reported that AI-generated code had been implicated in a series of outages — including one that took down Amazon’s entire e-commerce website for several hours. Amazon’s response was to deny the problem existed, which is the corporate equivalent of the AI itself: confidently wrong and hoping nobody checks. James Gosling, the creator of Java, who left AWS in 2024, was less diplomatic. He observed that the company’s AI-driven restructuring had “demolished” the teams responsible for infrastructure stability, and that the ROI analysis behind the decision was, in his words, “disastrously shortsighted.” One does not need a diagnostic engine to identify the fault here. A company replaced the engineers who understood its systems with a technology that does not, and the systems fell over. The circuit breaker that the AI removed — the one it classified as “redundant” — had been added after a previous outage. The AI could not distinguish a safety mechanism from dead code, because it had no model of the system. It had statistics. Statistics told it the breaker rarely fired. A model would have told it why.

    This is the difference between machine learning and model-based reasoning, and it is the difference that this post — and the toolchain I am releasing today — is about.

    An Unexpected Reception

    Yesterday’s post announcing qbf-designer, a tool for exact digital circuit synthesis via Quantified Boolean Formula solving, generated rather more attention than I had anticipated. Twenty-two thousand LinkedIn impressions, a hundred-odd reactions, and five hundred profile views in twenty-four hours, for a post about problems at the second level of the polynomial hierarchy and FPGA technology mapping. One concludes that there is an audience for work that produces correct answers, even — or perhaps especially — in an era when the prevailing technology cannot reliably tell you which end of a circuit is up.

    Dusting Off the Arsenal

    To continue with my plans for commercialising formal methods for EDA through Llama Logic Corporation, I have to excavate, modernise, and release the full inventory of tools and concepts I have built over nearly two decades. There are many reusable components in this stack — logic representations, solver bindings, encoding schemes, diagnostic algorithms — and they need to be cleaned up, documented, and made available. The qbf-designer release was the first. Today’s is the second.

    Today I am releasing LyDiA, a language and toolchain for Model-Based Diagnosis. LyDiA was the core of my doctoral research at Delft University of Technology. I will not be using LyDiA itself going forward — the modern llogic packages have fixed all of its imprecise notions and provide a cleaner foundation for everything I am building — but LyDiA was where it all started. It was my first serious work on the diagnosis of circuits, and it contains ideas and algorithms that remain relevant. It deserves to be available.

    Model-Based Diagnosis in 15 Seconds

    The demo takes two inputs. The model (2adder-weak.sys) describes a two-bit full adder — a hierarchical composition of half-adders built from XOR and AND gates. Every gate has a Boolean health variable: true means the gate works correctly, false means it is faulty and its output is unconstrained. We do not specify how a gate fails, only that its output can no longer be trusted. This is called a weak fault model.

    The observation (2adder.obs) records what actually happened: specific values on the inputs and outputs of the circuit that are inconsistent with correct behaviour. Something is broken. We do not know what. The diag command hands both files to the GOTCHA engine — which computes all minimal sets of component failures that explain the discrepancy. Not one guess. Not the most likely answer. Every combination of gate failures that is logically consistent with the model and the observation, with no redundancy.

    The fm command lists the results: six double-fault diagnoses, each a minimal set of gates whose simultaneous failure is sufficient to produce the observed misbehaviour. For example, d4 = { !FA.HA1.X.h, !FA.O.h } means the XOR gate in the first half-adder and the OR gate are both broken. There is no single-fault explanation — at least two gates must be faulty, and the engine has proven this by exhaustive enumeration.

    Why Circuits?

    Writing software to diagnose a fabricated IC does not make practical sense. You would use ATPG and scan chains for that. We use digital circuits as benchmarks because they have the properties that matter for diagnosis research: compositional structure, many components, well-defined fault models, and known-correct reference behaviour. These are the same properties that make diagnosis hard in complex engineered systems generally. This is why the ISCAS-85 suite has been the standard MBD benchmark for thirty years.

    Where diagnosis does apply directly in EDA is design verification. Suppose an engineer places a NAND gate instead of an AND gate for the carry computation in the adder above. The circuit passes some tests but fails on specific input vectors. The diagnostic engine, given the intended specification and the observed misbehaviour, will isolate the carry gate as the faulty component — even if the designer has never seen this particular mistake before, even if there are multiple simultaneous design errors. It reasons from the structure of the circuit, not from a database of past bugs.

    The Modelling Problem

    During my early attempts at commercialisation, I encountered a pattern that I suspect anyone in formal methods has seen. People looked at LyDiA diagnosing circuits and said: “Wonderful. Can it diagnose my HVAC system? My chemical plant? My supply chain?” And so they tried to model non-circuits as circuits, and things did not work, because the difficulty of modelling is the hard part.

    Circuit diagnosis is tractable in part because digital circuits have a natural, compositional, Boolean structure. An AND gate is an AND gate. An HVAC system is a tangle of continuous dynamics, feedback loops, thermal gradients, and human behaviour. Cramming that into a Boolean framework requires heroic abstraction, and the resulting models are either too coarse to be useful or too large to be solvable. The aerospace fuel system model included in LyDiA — with its typed fault modes for leaking tanks, stuck sensors, and degraded pumps — hints at what multi-valued modelling can achieve, but it remains a toy compared to the real thing.

    That said, LyDiA was never only about circuits. The distribution includes models of the N-queens problem, map colouring, Sudoku, and SEND+MORE=MONEY — general constraint satisfaction problems expressed in the same language. The diagnostic framework is, at its core, a constraint solver with a notion of health variables. This generality is both its strength and its curse: it can express anything, but making it useful for a specific domain requires domain expertise that no tool can substitute.

    What LyDiA Got Wrong: Probability

    LyDiA assigns fault probabilities to components — each gate gets a prior like 0.99 healthy, 0.01 faulty — but the probabilistic reasoning was never worked out correctly. The probabilities were treated as independent priors, multiplied together to rank diagnoses, with no rigorous account of how observations update beliefs or how correlations between faults propagate through the system.

    The correct formulation turns out to be a #P problem — a counting problem. To compute the exact posterior probability of a diagnosis, you need to count the satisfying assignments of the diagnostic formula: how many ways can the internal signals of the circuit be assigned such that the model, the observation, and a given fault assumption are all consistent? The probability of a diagnosis is the ratio of its satisfying assignment count to the total. This is model counting, and it is #P-complete — harder than NP.

    One consequence is that all diagnostic probabilities are rationals. They are ratios of integers — counts of discrete satisfying assignments. This has some puzzling implications for the relationship between fault probability and physical failure rates that I have not yet fully worked out.

    There is also a quantum angle. Faults are inherently stochastic — a gate either works or it does not, and before you test it, the fault state is indeterminate in precisely the sense that a qubit is indeterminate before measurement. I showed in earlier work that placing health qubits in superposition and propagating them through a quantum circuit that mirrors the classical circuit under diagnosis computes the full probability distribution over all diagnoses simultaneously. This connects to von Neumann’s foundational work on the relationship between logic and probability. The practical implication is Grover’s algorithm: a quadratic speedup for searching the diagnostic space. I need to finish this work and implement a proper Grover-based diagnostic engine. It is on the list.

    Why Machine Learning Cannot Do This

    In February, a company called Algorhythm Holdings — formerly a manufacturer of karaoke machines, with a market capitalisation of six million dollars — announced that its AI platform could “optimise” freight logistics, scaling volumes by 300–400% without adding staff. The announcement wiped seventeen billion dollars off U.S. transportation stocks in a single day. C.H. Robinson fell 15%. RXO fell 20%. The Russell 3000 Trucking Index dropped 6.6%. DHL, DSV, and Kuehne+Nagel followed in Europe. All of this because a former karaoke company claimed, in effect, to have solved optimal planning — a problem that is PSPACE-complete. If Alan Turing and Stephen Cook could be reached for comment, I suspect they would have questions.

    The same magical thinking pervades “AI for diagnostics.” A machine learning model trained on historical failures will recognise patterns it has seen before. Show it a novel fault — a combination that never appeared in the training data — and it has nothing to generalise from. It will either misclassify the failure or express high confidence in a wrong answer. This is not a limitation that more data or a larger model can fix. It is a structural property of inductive inference: you cannot learn what you have not observed, and complex systems fail in ways that are combinatorially vast and fundamentally unpredictable from examples alone.

    Model-based diagnosis does not have this problem. If you have a model of the system, you can diagnose faults you have never observed, in configurations you have never tested, because the reasoning is deductive rather than inductive. The SAT solver asks: is there an assignment of health variables that is consistent with the model and the observations? The answer is provably correct with respect to the model. This is why NASA uses model-based diagnosis for spacecraft and why the automotive industry uses it for on-board diagnostics. Nobody uses a neural network to diagnose a flight-critical system. The neural network might get it right 95 percent of the time. The other 5 percent is a smoking crater.

    What’s Next

    The modern diagnosis packages in llogic have addressed all of LyDiA’s imprecisions — cleaner encodings, correct probabilistic inference, proper multi-valued support — but those are a story for a separate post.

    There is also Lydia-NG, a framework I built that extends model-based diagnosis to analog systems using a built-in SPICE simulation engine. Rethinking Lydia-NG connects us directly to the analog side of EDA — a domain where formal methods have barely made an appearance and where the tools are, to put it charitably, showing their age.

    And that is the longer ambition. Cadence Virtuoso dates from 1991 — thirty-five years old. Vivado is newer (2012), but its place-and-route lineage descends from NeoCAD, acquired in 1995, and its synthesis from MINC, acquired in 1998. Synopsys Design Compiler has been around since the late 1980s. The EDA industry is running on architectural foundations that predate the web browser. These tools work — in the sense that a 1991 Toyota also works — but the algorithms inside them are heuristic, the interfaces are hostile, and nobody has rethought the fundamentals in decades.

    The goal of Llama Logic Corporation is to challenge this. Modern EDA with proper AI-augmented formal methods — analog, digital, and FPGA. New languages. New solvers. New tools. Not “AI for EDA” in the Silicon Valley sense of wrapping an LLM around Verilog and hoping for the best, but the real thing: algorithms with correctness guarantees, backed by the mathematical foundations that already exist and that the industry has been too comfortable to adopt.

    In the next instalment, I will demonstrate qbf-designer doing FPGA technology mapping — covering a small circuit with k-input Look-Up Tables. The formal methods stack is growing. The software works. It does not hallucinate.

    The repository: LyDiA — language and toolchain for Model-Based Diagnosis.

  • The Synthesis Problem: Why I’m Building a New Logic Toolchain

    Modern chip design leaves performance on the table. A lot of it. Meanwhile, billionaire CEOs with the technical depth of a drunk high-schooler who wants to be new age when he grows up keep calling a glorified autocomplete “AGI.” Nobody’s asking if the circuit itself is well-designed — just whether the output sounds smart.

    The tools we use to go from a logical specification to a physical circuit are decades old in their core ideas. They work — billions of transistors ship every year — but they settle for “good enough” at almost every stage of the pipeline. Synthesis heuristics that don’t explore the real optimization space. Representation formats that can’t talk to each other. A wall between the people who study formal logic and the people who tape out silicon.

    I want to build better circuits. Not a better CPU, not a better GPU — better circuits, generally. Classical, reversible, quantum. The kind of improvement that comes from rethinking the synthesis process itself, not from adding more transistors.

    That’s what this project is about.

    What I Actually Built

    Over the past several years, I’ve been assembling an open source toolchain that connects formal logic to real hardware. Each piece exists because I hit a wall with existing tools.

    llogic is the foundation — a library of logic representations. Boolean formulas, CNF, DNF, OBDDs, QBF, combinational circuits, reversible circuits, quantum circuits. They all live under one roof because they share more structure than the textbooks let on. A circuit is a formula is a constraint problem. If your tools understand that, you can move between representations and optimize across them.

    lcfgen generates circuit families — parameterized circuit structures that let you explore design spaces systematically instead of hand-wiring one instance at a time.

    llogic2verilog translates circuits from llogic’s internal representation into synthesizable Verilog. This is the bridge from formal logic to hardware toolchains.

    lverilog is a Verilog parser that produces a clean AST, because I needed one that I could actually inspect and transform programmatically without fighting a legacy codebase.

    llogic_basys3 is the proof that this isn’t academic exercise. It targets the Digilent Basys3 board — a Xilinx Artix-7 FPGA — and runs brute-force integer factorization by testing 16×16 bit multiplication at 50 MHz. A MicroBlaze soft processor drives the circuit over AXI, exposed as a UART interface. You feed it a number, it searches for factors — on a $150 hobby board, clocking through candidates at 50 million per second.

    Theory in. Hardware out. No marketing budget required, no claims of sentience.

    Why This Matters

    The connection between Boolean satisfiability, quantified Boolean formulas, and circuit structure is well-studied in theory. My published work on QBF-based circuit synthesis showed that you can use the structure of quantified formulas to derive circuits with provable properties. But the research community largely stops at the paper. The tooling to go from that theory to running hardware didn’t exist.

    It does now.

    And the scope is broader than classical digital logic. The same formal framework that represents a combinational circuit can represent a reversible circuit or a quantum circuit. The same optimization that simplifies a Boolean formula can simplify a quantum algorithm’s gate structure. There’s a deep connection to Bayesian inference here too — probabilistic reasoning over circuit structure — that I’ll write about separately.

    Where This Goes

    I’m not building a toolchain for the sake of building a toolchain. I care about two things: scalability and energy efficiency. Better synthesis means smaller circuits. Smaller circuits mean less power, less area, more throughput. At scale, this is the difference between a computation that’s feasible and one that isn’t.

    The implications reach beyond hardware design. Optimized circuit structures have direct applications in machine learning acceleration — which is to say, making the very large circuits that people mistake for intelligence actually run efficiently. The same goes for cryptanalysis and scientific computing — anywhere you’re bottlenecked by the gap between what you want to compute and what the hardware can deliver. I’ll write about those connections in future posts.

    The FPGA demo is the first milestone — a hobby board factoring integers to prove the pipeline works end-to-end. The next steps involve pushing the optimization boundaries, extending to quantum targets, and making the case — with working hardware — that this approach produces better circuits.

    If you’re a researcher working on synthesis, a hardware engineer frustrated with your tools, or a program manager looking for the next leap in design methodology: let’s talk.

    The code is open source. The results are reproducible. The ambition is to build circuits more powerful than anything that exists today.

    Repositories: