Have become top 3 trending developer on Github, with @mitchellh right behind me 😱

We found that transferred filenames could place raw control characters into rsync logs. A filename entered as data. When an administrator later opened the log in a terminal, those bytes could become terminal escape sequences. rsync now escapes them.

I was talking with people who work in factories. Not people who write software for factories. They told me they don't trust software engineers. They'd seen a model that worked on paper fail on the floor. Dust on a sensor. A replacement part from a slightly different batch. A machine that behaves differently on a cold morning than it did during acceptance testing.

Django has a comment that basically tells you to stop thinking: if the other Q() is empty, ignore it and just use self. The implementation deep-copies the object. Combining an empty Q() with Q(x__in={}.keys()) raised TypeError: cannot pickle 'dict_keys' object. An empty query, which was supposed to contribute nothing, added a new requirement: the other side had to survive copying.

Code used to be expensive to produce, so it became the main asset. I can get a lot of it now for almost nothing. The files still compile. Intent is the part that gets easier to lose.

Django builds a hashed filename like this: if file_hash is not None, prefix a dot, then glue root + hash + ext. When a custom hash returns None, styles.css becomes stylesNone.css. No exception. A valid string with the wrong name. The check is sitting right there, naming the value that breaks it, then turning that None into text.

I would still pay twice as much for Claude Code and Codex. As an individual the economics work. If it increases my output, I keep paying. A product business is different. I don't want the whole margin sitting in the model bill.

Trail of Bits worked the same rsync 3.5.0 release I was on. They found issues we didn't. We found issues they didn't, including some that had survived for decades. In ten cases, since the first release in 1996.

We got spoiled by Claude Code and Codex. After using them, going back hurts. You start expecting the model to keep the context and behave like a useful partner. Then I try the open-source ones. Some look close to Opus on the benches. In the actual work they are not. Bugs, edge cases, a harness that was never tuned for them.

Django's number formatter turns 1e25 into "1e+25". There's no decimal point, so the whole string becomes the integer part. The grouping loop then walks those characters and inserts a separator every three positions. In the environment I audited that produced '1e,+25'. A thousands separator inside the exponent. Naming it int_part didn't make those characters digits.

I can move incredibly fast as an IC now. I open Claude Code, give it direction, and the real decisions happen while the code is being written. I try something. I see what it did. The original idea was wrong. I adjust. That loop works while the system still fits in my head. The source of truth there is me, not the files.

Telling the AI agent to generate the formal proof contract based on the code is basically the same as telling the AI agent to review the code. They shake hands with each other, but who would validate that the Lean contract is correct? With time any product grows with edge cases, some if spaghetti, and so on, and the code never tells you why. It tells you only what, and the why thing usually lives in Jira, in the commit history, etc. In order to answer it, you need to do the proper data archaeology behind it. We, as humans, usually do it this way. This approach of generating the Lean, for sure, will be able to show a lot of bugs, but a lot of them will also be noise because of the contract misunderstanding. Who is going to filter through this noise? Again, probably some agent, and we have this weird loop: who is responsible for defining how the application actually is supposed to behave? It definitely should be the human. What is the source of truth here? Is it the code, or is it the Lean contract? Is it a one-time job, or is it going to support both implementation and the contract in parallel while you are writing it? The right way to way to introduce formal verification is to look into the root cause first: the code itself stopped being the source of truth. It's a temporary artifact, same as a tests. The source of truth should be some requirement management system managed by the humans who define what the software is, how it should behave, etc. The rest, the code, the tests, and the contracts are attached as evidence which proves these requirements. Basically, what I described is exactly how software engineering is done in regulated industries.

One of the rsync requirements looked almost embarrassingly simple. A host matching hosts deny must not be admitted. The check failed. When a hostname in a deny rule could not be resolved, rsync skipped the rule. Under that config it failed open. That became CVE-2026-70452, rated HIGH.

When I tried weaker models they didn't forgive a lazy prompt. They don't magically understand what I meant. They expose the bad context, the unclear task, the missing boundary. A strong model can hide a lot of that. That's why I still run the cheap ones on purpose.

I asked GLM-5.3-flash to find bugs by looking at the code, no clues. Across three versions of the review instructions it found none of the seven selected hard defects. Zero out of seven each time. One experiment required line-by-line traces. Thirty-eight of the forty-eight outputs followed that format. The missing findings still did not show up.

If a model can disappear in three days, so can the harness around it. I started building my own. Probe for search. Visor for the review workflow. Not because I enjoy making my life more complicated, although I do. I want to own how context is prepared and how the model is called.

This summer I went back to jsonparser after ten years. Six releases. 50 open issues and 12 open PRs down to zero. 12 real bugs fixed. Zero breaking changes. I went back to make the "fastest" claim true again.

When the agent writes the code, my job is still the mismatch. What we wanted, what we specified, what got implemented, and the world it actually runs in. Those four are rarely the same sentence. I used to catch "don't charge twice" while I was typing. Now I have to catch it in a PR I didn't write.

A few hundred candidate reports went through the rsync 3.5.0 cycle. We filed 99 findings. 28 were later withdrawn. The release shipped with 33 security fixes. Those are three different numbers. The distance between them is where most of the work happened. A report can take five minutes to generate. Deciding whether it is real still takes hours.

I don't need a smarter model. I need more sessions. I already pay about $700 a month across five accounts. Codex, two Claude seats, a couple of hosted ones. My output is limited by how many high-quality runs I can start before I hit a cap. Opus and Codex already do almost everything I wanted. If I had cheap, almost unlimited access to that level, I could do a ridiculous amount of work with what already exists.

I got some GTM advice from an experienced sales person that changed how I position Proof, the project I’m building - and how I see it. I started the call with a complex explanation about bringing regulated engineering practices into our world, with all the nuances. The person on the other end was clearly very patient... and luckily knew a few terms, like requirements management. Then came the question: “What jobs do you remove, and how much money do you save?” Such a simple idea, but so hard to process. We as founders get so deep into the details that we forget: the customer needs a pain solved and money saved. How you do it matters much less than we think. All these fancy words—formal verification, requirements management, etc.—sound like things the team has to learn and put on top of existing processes. You think you’re explaining the solution. They hear more work. The same thing happened when I pitched Proof as something that would find and fix all your logical and security bugs. The response was: “We’re already drowning in bugs, and you’re offering us one more channel of them?”. And in the end it is not about having product without bugs - it is about having product you trust. Another recommendation I was given: forget about developer happiness as the pitch. No one really cares; the final decision sits with the CFO. If you can convince them they can get the same result with 30% less work, that’s what matters - even if it may mean firing some people. That’s how business works. And moreover, pitching developers or QA - even in senior positions - a tool that could reduce QA time and regression work by an order of magnitude can get sabotaged. You’re offering to remove work. They may hear that you’re offering to remove their job. Why would they want to dig their own grave? For this kind of pain, the solution may need to come from the top down - unlike all the projects I’ve worked on before. So what exactly I have changed in my pitch? So far, it looks like this: Proof reduces the work between a software change and the evidence required to trust it. Every consequential software change - whether made by a person or an agent - should carry its intent, blast radius, evidence, authority, and limitations with it. What work it removes or make easier? 1. Less human engineering time per accepted change. 2. Less regression and rework effort. 3. More work safely delegated to agents. Hope this got you thinking, and maybe a little curious :)