nemo1618

That's the nice thing about the approach described in the blog: you use the same Rocq theorem for every binary (it just says "this binary doesn't crash") and then you express the property you want in your language of choice. For example, to prove that your compression algorithm round-trips, you would write something like assert(x == decompress(compress(x))).

In essence this lets you verify any property you want for a given function, as long as it can be expressed as a fuzz test. Specifically, you can express your property with an assert, and then prove that it never fires. This is nice because it keeps everything in one language, rather than having to translate the whole program into Rocq and then express your desired property as a Rocq theorem.

I think it's a really illustrative example of how to play to AI's strengths. No human would dream of writing 600,000 lines of Rocq to verify one binary. The whole approach is so insane that it probably wouldn't even occur to them. But Claude has no concept of tedium, and will happily fill out lemmas all day long until the job is done. To me that's what's significant about this result: it's not about scaling up an existing technique, it's about using scale itself as the basis of a new technique.

It warms my heart to see so many people in the comments clarifying that LLMs can indeed be deterministic. This was not always the case!

I hope that we will soon see deterministic inference offered by frontier labs (presumably at a premium rate). In the meantime, you can get deterministic behavior from local models using the right vLLM flags. I've described some of the cool applications of determinism here: https://lukechampine.com/repligraphs

Thank you for the kind words! It's funny how much staying power those blog posts have, haha. Michael has some arcane ability to consistently hit the front page of HN.

True, I expect models to be pretty correlated with each other as well. But you can at least attempt to quantify that correlation in a rigorous way, by running experiments (e.g. by pointing each model at a big project and comparing the sets of bugs they each find).

And yeah, the "double-edged sword" aspect of determinism is definitely the biggest bullet that you have to bite. For me, it's better than the alternative; without determinism, such jailbreaking attacks are still possible, just harder to detect. But I certainly would not want people to go around thinking "it's deterministic, therefore it's safe."

LLMs can be deterministic too! People just don't bother because the applications of this aren't widely known yet. See https://lukechampine.com/repligraphs

True, you can't do this with GPT or Claude, at least not today. But you can do it with a local model: vLLM supports deterministic inference out of the box! (If you have a MacBook, you can confirm this yourself; just point your agent of choice at the site. It will download a small open model and run it with vLLM Metal.)

Naturally, I hope that OpenAI and Anthropic will one day offer deterministic inference; see the "Weights" page for what this might look like.

I had a similar idea for Super Smash Bros Melee! There is a lot of very low-quality footage out there; surely you could train some sort of model to convert it to Slippi replays. A year or two ago this would have been a grad student project; a year or two from now, it will be a one-shot prompt.

Even at Burning Man, in the middle of the desert, there is a camp that hosts a StarCraft tournament every year (on the dustiest setups you've ever seen!) :)

Your assumption is mistaken (and a little rude).

I love programming. It's in my blood: my father and grandfather were programmers too. I have written everything from SIMD assembly to Hoon, and implemented several languages of my own. Believe me, I am intimately familiar with the phenomenon you are describing.

It's true, the devil is in the details. And I will grudgingly concede that, at present, humans are better at exorcising demons than AI. But I see no reason to believe that this will remain true. The gap is narrowing rapidly, and even today there are types of demons that AI can dispatch much more quickly and effectively than you or I can. The fact that vibe coding is possible at all (and that people are willing to pay for vibe-coded apps) is proof that an informal English prompt is sufficient to specify software to an acceptable degree. Not acceptable to everyone, naturally, but at least to the creator and the users.

I am not exactly happy about this. It is bittersweet. Much of my identity is bound up in being a programmer. The devil is in the details; but joy and whimsy and great beauty are in the details as well. For a glorious few decades, one could be an artist under the guise of producing economic value. Now, the economic aspect of producing software is being siphoned off, to be done by machines, leaving only the art. I think we will suffer for that, somewhat. But it is a small price to pay.

Further evidence that there is some kind of weird parallel universe thing going on with LLMs. "Figuring out esoteric errors" is one of the things I would cite as a particular strength of agents. I am repeatedly amazed at their ability to root-cause weird behavior on my systems. Here is one example: https://xcancel.com/lukechampine/status/2047032091053859138

I am quite tired of this take, frankly. The implication is that if we continue iterating on prompt optimization, we're going to reinvent what, JavaScript? BASIC? Lisp?

English is not a programming language. Yet English is sufficient to communicate requirements to the degree that we actually care about. A programmer's job is to translate English into lower-level machine language. Necessary to this process is "filling in the gaps" -- that is, extrapolating the expressed intent to cover all the little details that were left unspecified. This system works because humans are at least minimally competent at predicting the preferences of other humans. If your prediction turns out to be wrong, you get feedback and iterate.

Well, guess what. LLMs are also competent at predicting the preferences of humans. LLMs can "fill in the gaps" like no one's business. LLMs can iterate on requirements like no one's business.

Product managers do not speak to programmers in a language that encodes exact requirements, and yet working software somehow gets shipped anyway. LLMs do not need exact requirements either.

After Christmas this year, I removed the tree from our living room, and in the process of being moved, it shed of needles everywhere. I swept them up, but I missed a few areas on my first pass. So I did a second pass, but when I looked again, I saw there were still a handful left. It struck me how removing >99% of the needles was nowhere near acceptable! Lots of cleaning jobs are like this, I suppose, because even a tiny mess can be visually distinct. In fact, as you approach 100%, the remaining mess stands out more.

I would love a crank-powered router. Would be a good way to curb internet addiction!

I think the key is that, while you may think you have a full formal spec of f(), you actually do not. You have a program written in some language, and that language has its own spec, and the language is compiled to asm which has its own spec, and the asm executes on an architecture that has its own spec, and so on.

So when you write a function like:

  func hypot(x, y):
    return sqrt(x*x + y*y)

You might think you have "fully specified" hypot, but this is far from true! You have said nothing about what registers will be used, for example. This is not a problem; quite the opposite. It's the whole point of using high-level languages: they let you focus on what you care about. A spec is just a program in a very-high-level language.

The first moment I specifically remember was writing a test of a new RPC protocol back in 2021. There were no agents yet, only "AI autocomplete" in the form of GitHub Copilot. I wrote the "server" half of the test, which received a name and responded with "Hello, <name>". Then I wrote the client code to send "world", and Codex suggested `if response == "Hello, world"`.

I was floored by this. How could it have known?!

We have come so far in such a short time.

It really is crazy. I have been contributing the Melee decompilation project for the past year-ish, and things have really accelerated in 2026. Just today I decided it would be nice to have a better "permuter" (program that randomly modifies C in the hopes of finding a better asm match) so I...just asked Claude to make one, custom-tailored to my needs. It almost feels pointless to publish it to GitHub when I can just tell the other contributors "hey fyi you can ask Claude to make you a better permuter"

You should not swear at LLMs, for the same reason you should not shout a slur even if no one is around to witness it: You witness it, and witnessing yourself being toxic updates you in the direction of "I am capable of toxicity" and eventually "I am toxic." In other words, it stains your soul.

Good git hygiene is also less important post-LLMs, as the LLM can make sense of even a messy history.

Agreed. In fact, one of the things I now watch for is my mind starting to "slide off" the text, or finding myself re-reading a section multiple times. It's like the brain subconsciously recognizes a lack of substance even if we can't point to a specific tell.

LLM writing tells are getting more subtle, but they still jump off the page for me, in particular the word "genuine:"

   "This is the area where Go genuinely shines, and it’s worth being precise about why"
   "the lack of GC pauses is a genuine selling point"
   "Humans are genuinely bad at reasoning about memory"
   "There are cases where the borrow checker is genuinely too strict"

tbc I don't think the article was fully AI-generated, just AI-assisted. If so, the author did a genuinely good job of it! No one else is commenting on it, so clearly it didn't detract much from the substance. It's just weird that this is becoming increasingly common, and increasingly hard to detect.

Evidence for 1992:

> After a disorienting visit from the FBI in May of 1990, I wrote a rant called Crime and Puzzlement, which led to my establishing with Mitch Kapor (who had previously founded Lotus Development Company) an organization called the Electronic Frontier Foundation.

> Now, after almost two years of operation...

It's interesting to revisit Brooks' "surgical team" in light of AI. For example, I frequently have Claude act as a "toolsmith", creating bespoke project-specific tools on the fly, which are then documented in Skills that Claude can use going forward. What has changed is that a) One person (or rather, one person-AI hybrid) plays all the roles within the surgical team, and b) Internal frictions such as cost, development time, and communication overhead have all been dramatically slashed.

Huh? I'm not aware of anyone else who defines "deterministic" that way. "Deterministic" comes from "determinism," as in "the effects are fully determined by the causes" -- not "determine" as in "deduce."

LLMs are not inherently non-deterministic. This is a common misconception. You used to be able to set temp=0 and a fixed seed and get the same output every time. This broke when labs started implementing batching, and no one bothered fixing it because the benefits of batching vastly outweighed the demand for deterministic output.

I am hopeful deterministic output will return, though; DeepSeek v4 claims to have implemented "bitwise batch-invariant and deterministic kernels," though I haven't tested it myself.

Sufficiently-developed concentration gives you access to the jhanas, which are extremely blissful states of consciousness. Having reliable access to high valence reduces your need to seek pleasure in less wholesome things (drugs, food, twitter, etc.)

Sufficiently-developed attention gives you insight into how your brain is constructing what you perceive as reality, leading to a reduction in ego, permanent reduction in baseline suffering, and a pervading sense of unity with the rest of the universe.

I'm old enough to remember when companies worth $1 billion were called "unicorns." Now we have a company raising 122 times that? Valued at nearly 1000 times that...?

At least they're throwing consumers a bone via the ARK deal. It's crazy how little AI exposure is available to anyone who isn't already wealthy and/or connected.

yep, I do a simple version of this in Google Sheets. Very useful to be able to "Ctrl-F" your life, especially when combined with Google Maps location history.

If this was a joke, it certainly flew over most people's heads...

This will happen with GUIs as well, once computer-use agents start getting good. Why bother providing an API, when people can just direct their agent to click around inside the app? Trillions of matmuls to accomplish the same result as one HTTP request. It will be glorious. (I am only half joking...)