Wikipedia article: https://en.wikipedia.org/wiki/Franklin_Electronic_Publishers

The "Last-Modified" HTML header suggests it was last updated on "Sat, 05 Jul 2025 04:27:21 GMT": https://celsoazevedo.com/files/2026/franklin-mod.png

> The two bugs that were found both sat outside the boundary of what the proofs cover. The denial-of-service was a missing specification. The heap overflow was a deeper issue in the trusted computing base, the C++ runtime that the entire proof edifice assumes is correct.

Still an interesting and useful result to find a bug in the Lean runtime, but I’d argue that doesn’t justify the title. Or the claim that “the entire proof edifice” is somehow shaky.

It’s important to note that this is the Lean runtime that has a bug, not the Lean kernel, which is the part that actually does the verification (aka proving). [1] So it’s not even immediately clear what this bug would really apply to, since obviously no one’s running any compiled Lean code in any kind of production hot path.

[1] https://lean-lang.org/doc/reference/latest/Elaboration-and-C...

If a buffer overflow causes the system to be exploited and all your bitcoins to be stolen, I don't think the fact that the bug being in the language runtime is going to be much consolation. Especially if the software you were running was advertised as formally verified as free of bugs.

Second, there was a bug in the code. Maybe not a functional correctness bug, but I, along with many and most end users, would consider a crashing program buggy. Maybe we just have different tastes or different standards on what we consider an acceptable level of software quality.

W.r.t people running Lean in production, you'd be surprised...

But it just moves the question to whether the theorems covered in the proof are sufficient. Underlying it all is a simple question:

Does the system meet its intended purpose?

To which the next question is:

What is the intended purpose?

Describing that is the holy grail of requirements specification. Natural language, behaviour-driven development, test-driven development and a host of other approaches attempt to bridge the gap between implicit purpose and explicit specification. Proof assistants are another tool in that box.

It's also one of the key motivators for iterative development: putting software in front of users (or their proxies) is still the primary means of validation for a large class of systems.

None of which is implied criticism of any of those approaches. Equally, none completely solves the problem. There is a risk that formal proofs, combined with proof assistants, are trumpeted as "the way" to mitigate the risk that LLM-developed apps don't perform as intended.

They might help. They can show that code is correct with respect to some specification, and that the specification is self-consistent. They cannot prove that the specification is complete with regards its intended purpose.

> The most substantial finding was a heap buffer overflow! but, not in lean-zip's code, but in the Lean runtime itself. (emphasis mine)

> The OOM denial-of-service is straightforward: the archive parser was never verified. (me again)

"Lean proved this program correct" vs "I found bugs in the parts that Lean didn't prove was correct". The failure was not in Lean's proof (which as I said is heavily implied by the title), but in ancillary or unverified code.

Do I misunderstand how Lean works? I am by no means an expert (or even an amateur) on Lean or formal systems in general. Surely the first class of bug could be found in any code that uses the framework, and the second class of bug could happen to any system that isn't proven? Does that make sense? Otherwise where's the boundary? If you find a bug in the OS, does that mean Lean failed somehow? How about the hardware? If your definition of a 'formally verified system' goes beyond the code being verified and the most important thing is whether or not you can make it crash, then the OS and the hardware are also part of the system.

Of course bugs are important to users regardless of the cause, but the audience for your article seems to be software engineers and as a software engineer, your article was interesting and you found something useful, but the title was misleading; that's all I'm saying.

- When they fix the run time, bug A goes away. So the proof still holds and the zlib code is still correct.

- When they add a system of proofs for the parser and modify that, then bug B goes away. So the proof still holds and the zlib code is still correct; and now more of the library is proven correct.

The formulation of the title is "I was told X but that's not true"... but that's not true. You were told X, and X is true, but you found Y and Z which are also important.

There are two different answers to this question, and which one is "correct" depends entirely on the context of who is asking it.

1. It's the code that is specific to this program that sits above the run-time layer (internal view, that most programmers would take).

2. It's the code in the binary that is executed (external view, that most users would take).

The key question does not seem to be "was the proof correct", rather "did the proof cover everything in the program". The answer depends on whether you are looking at it from the perspective of a programmer, or a user. Given the overly strong framing that the article is responding to - highlighting the difference in this way does seem to be useful. The title is correct from the perspective that most users would take.

My feeling is that if you told the average non-technical user that some person/organisation had produced a formally verified version of a C compression library, you would likely get a blank look, so I think it's reasonable to assume that both Lean's intended audience, and the audience of the blog post linked here, correspond with number 1. in your list.

The bounded, specific codebase that you refer to is typically the library *and all of its dependencies*, which in this case includes the Lean runtime. This is why formal verification is difficult: the proof chain needs to extend all the way down to the foundations. In this case the original gushing claim that everything was verified is incorrect and premature. The article seems like a good exposition of why.

> The bounded, specific codebase that you refer to is typically the library and all of its dependencies, which in this case includes the Lean runtime.

How does that work? I thought the main idea is to write code in the Lean language which has some specific shape conducive to mathematical analysis, along with mathematical proofs that operate on that code. How then does a system like this handle a third party dependency? I've searched around and I can't find any information about how it works. I assumed that the boundary of the proof was the source code - surely they can't also be proving things like, say, DirectX?

> This is why formal verification is difficult: the proof chain needs to extend all the way down to the foundations.

The difficulty is not in explosions of computational complexity due to problems of incompleteness, decidability, the halting problem, those kinds of things? As I said this is not something I know much about but it's surprising to me if 'analysing all the code' is really the difficult bit.

As with most engineering problems the out-of-band issues tend to be the hardest to solve. Models of the part underneath the interesting part need to be complete/accurate enough to make the results useful. Compare it to crypto where people do not usually try to break the scheme - they try to break the specific implementation of the scheme because the weakest points will be at the interface between the theoretical construction and the actual concrete instantiation of the device that it will run on.

> Please don't comment on whether someone read an article. "Did you even read the article? It mentions that" can be shortened to "The article mentions that".

Would you publish a blog post titled "the XXX test suite proved there was no bug. And then I found one"?

It would be a bit silly, right?

But yes, it would be equivalent to stating "No tests failed but I found a bug" and one would correctly deduce that test coverage is insufficient.

- testing libraries (and in this case - language itself) can have bugs

- what is not covered by tests can have bugs

Additionally would add that tests verify the assumptions of coder, not expectations of the business.

To give benefit to the author - I'd read the article as: having tests for given thing ensures that it does the thing that you built the tests for. This doesn't mean that your application is free of bugs (unless you have 100% coverage, can control entire state of the system, etc) nor that it does the right thing (or that it does the thing the right way)

Eg. something as simple as

  function foo(url) {
     data = fetch(url);
     return data;
  }

Basically, any non-functional side-effect behavior is a source of semantic "hiding" when measuring test coverage by lines being executed, and there is usually a lot of it (logging is another common source of side-effects not tested well). Some languages can handle this better with their typing approaches, but ultimately, there will be things that can behave differently depending on external circumstances (even bit flips, OOMs, full disk...) that were not planned for and do not flow from the code itself.

By way of analogy, if there was an article saying "I bought a 1Tb drive and it only came with 0.91 terabits", I think if you started explaining that technically the problem is the confusion between SI vs binary units and the title should really be "I bought a 0.91 terabit drive and was disappointed it didn't have more capacity", technically you'd be right, but people would rightfully eyeroll at you.

I take some comfort from being technically correct though; it's widely accepted by all of us pedants that that is the best kind of correct ;-)

I agree, but it’s not fair to imply that the verification was incorrect if the problem lies elsewhere.

This is a nice example of how careful you have to be to build a truly verified system.

Yes, and that would be relevant if this was a verified software system. But it wasn't: the system consisted of a verified X and unverified Y, and there were issues in the unverified Y.

The article explicitly acknowledges this: "The two bugs that were found both sat outside the boundary of what the proofs cover."

Reminds of what some people in the Rust community do: they fight how safe this is or not. I always challenge that the code is composed of layers, from which unsafe is going to be one. So yes, you are righ to say that. Unsafe means unsafe, safe means safe and we should respect the meaning of those words instead of twisting the meaning for marketing (though I must say I heard this from people in the community, not from the authors themselves, ever).

Let me rephrase: aside from that one example from a couple years ago, I haven’t seen any examples of production code written in Lean. I’d be very interested in being proven wrong, this isn’t something I desire, just what I’ve observed. Have you seen any others?

More generally, you implicitly make a good point: writing important libraries in Lean and calling in from another language is probably the most likely use case. So not programs / apps / binaries written in Lean, but small critical components.

> ... converted zlib (a C compression library) to Lean, passed the test suite, and then proved that the code is correct.

> Not tested. Proved. For every possible input. lean-zip

When I see a title transitioning from "Lean said this proof is okay" to "I found a bug in Lean", I'm intuitively going to think the author just found a soundness (or consistency) issue in Lean.

Still good to have found, but drawing conclusions past “someone could cheat at proving the continuum hypothesis” isn’t really warranted.

To illustrate, let's say you want to verify a "Hello world" program. You'd think a verification involves checking that it outputs "Hello, world!".

However, if a contractor or AI hands you a binary, what do you need to verify? You will need to verify that it does exactly print "Hello, world!", no more, no less. It should write to stdout not stderr. It shouldn't somehow hold a lock on a system resource that it can't clean up. It cannot secretly install a root-kit. It cannot try to read your credentials and send it somewhere. So you will need to specify the proof to a sufficient level of detail to capture those potential deviations.

Broadly, with both bugs, you need to ask a question: does this bug actually invalidate my belief that the program is "good"? And here you are pulling up a fact that the bug isn't found in the Lean kernel, which makes an assumption that there's no side-effect that bleeds over the abstraction boundary between the runtime and the kernel that affects the correctness of the proof; that safety guarantee is probably true 99.99% of the time - but if the bug causes a memory corruption, you'd be much less confident in that guarantee.

If you're really serious about verifying an unknown program, you will really think hard "what is missing from my spec"? And the answer will depend on things that are fuzzier than the Lean proof.

Now, pragmatically, there many ways a proof of correctness adds a lot of value. If you have the source code of a program, and you control the compiler, you can check the source code doesn't have weird imports ("why do I need kernel networking headers in this dumb calculator program?"), so the scope of the proof will be smaller, and you can write a small specification to prove it and the proof will be pretty convincing.

All in all, this is a toy problem that tells you : you can't verify what you don't know you should verify, and what you need to verify depends on the prior distribution of what the program is that you need to verify, so that conditional on the proof you have, the probability of correctness is sufficiently close to 1. There's a lesson to learn here, even if we deem Lean is still a good thing to use.

Every time someone makes this point, I feel obliged to point out that all alternatives to software verification have this exact same problem, AND many, many more.

https://kirancodes.me/posts/log-who-watches-the-watchers.htm...

You can see the clickbaitiness increases over time.

You're strawmanning the original authors' argument. The creator of lean-zip said that they proved there are no implementation bugs in the lean-zip program. A bug in lean-runtime does not contradict this claim.

If they e.g. specially crafted a .zip file that caused it to flip bits via row-hammer like memory accesses, the same would be true.

Ignorant question: why not? Is there an unacceptable performance penalty? And what's the recommended way in that case to make use of proven Lean code in production that keeps the same guarantees?

Also, part of my confidence comes from both having been a professional programmer for decades, across many languages, and also having programmed in Lean. It’s a great language for math, perhaps the best choice right now. But as a general purpose language it’s incredibly quirky.

Well, Lean is written in Lean, so I am pretty sure a runtime bug like this could be exploited to prove `False`. Yes, since the kernel is written in C++, technically it's not the part affected by this bug, but since you cannot use the Lean kernel without the Lean compiler, this difference does not matter.

I used to be sympathetic to complaints about not wanting to pay the developer account fee. But when you’re vibe coding, you’re probably paying a good chunk of change to your LLM supplier of choice every month, and the yearly developer account fee seems minor in comparison

Also, it’s just such a bad security precedent. This page describes the error you get as “the typical macOS Gatekeeper warning”, as though it were just another piece of corporate silliness, like clicking through a EULA.

Anyway, I don't see a problem with getting it out the door. People can just choose not to install it if they don't like it. I mean that's the whole idea of being early anyway, isn't it? Don't like a crappy bodged together UI? Don't like a lack of support? Don't like an unsigned app? You can wait until it has those things according to your preferences. In the meantime, the creator gets real users and feedback ASAP.

Right now it's closed source binary with a big fat "DOWNLOAD FOR FREE" button and instructions casually telling you to disable the last barrier between your system and persistent malware. Nobody should recommend this to anybody

Is that a US thing? Because in the UK you just get one for free - Companies House sends the info over to them, and a couple of days later it is available to search

[0] https://support.pushpay.com/s/article/Acquire-your-D-U-N-S-n...

Where are these displayed?

I see vagueposting has found its way into HN.

> I don't know how obvious it is these days, but the default path through D&B's website is the terrible one. They will try to extract money from you and harass you forever. You had to find Apple's own embedded form for it by using their search and going through some flow.

I just downloaded your app and ran it through hopper. There is a LOT of embedded Apple Script. I would never run an app like this with SIP disabled or without an active network blocker.

Your app requires direct access to major OS components: code signing, even during alpha should be a requirement.

It is my machine and I paid for it, why does the OS care about what I do with it? The only thing this leads to is making sure your customers grow into good little lemmings.

For everyone else it's probably sane to have it, works as a decent filter so someone not tech-savvy don't get hurt by installing malware disguised as an app, one would just need to state incredible features that almost any normal user would like to have, and make them click to install. Gatekeeper diminishes that risk by a lot unless you learn how to bypass it, which requires you having decent skills and probably wouldn't fall for the bullshit that malware apps try to bait people with.

Full stop. I still talk to people every working day who don't realize that rebooting a computer is actually a real troubleshooting step. They seem to think it's bunk tech support mumbo jumbo rather than a genuinely useful step. It's 2026 and they're still surprised when that works.

It indeed is. It's a way of coping with systems that are fundamentally illegible and unpredictable. If you have full rights over your machine and you're not running extremely shoddy software, you should never have to reboot your computer to make an issue go away. And rebooting your computer often guarantees that you'll never actually understand whatever issue is plaguing you.

Encouraging people to reboot their computers is promoting a fundamentally superstitious mode of engagement with machines that are generally reliable and predictable, instead of approaching them in terms of cause and effect. At best, it's the tired point-and-click sysadmin's workaround for not knowing what their system is doing.

Maybe for overwhelmed IT departments running half-baked operating systems loaded to the gills with invasive and meddlesome corporate spyware suites so inherently complex and complicated in their interactions with each other that the system itself is rendered more or less incomprehensible (even to the people administering it), just asking users to reboot is the right play to write in the tech support playbook. Maybe it's got the right ROI for a geek reluctantly roped into giving free tech support for a relative. But it's absolutely mumbo-jumbo and a sign that the "troubleshooter" is probably either ill-equipped to understand what's going on or just not interested.

About two weeks ago, some Adobe Acrobat update introduced a hang that results in “Acrobat won’t open.” Open Task Manager and there’s four to eight stuck processes. Kill them and it works again most of the time, but once in ten it simply doesn’t recover.

Adobe acknowledged the issue to someone on my team. There’s no need for me to understand further; telling the user that a reboot will solve it is prudent advice. It’s on Adobe to fix it. You made assumptions about the environment where I tell people to reboot without understanding the conditions and I have an immediate real world case demonstrating why your statements don’t apply.

It's like you are saying that potentially dangerous tools shouldn't have safety guards whenever possible, with little impact for the common use of the tool. Kinda absurd to think that way... If some advanced use-cases require safety guards to be removed that's when the user should be trained enough to know the risks.

People want to use a computer for their tasks, the whole motto of Apple was to make technology accessible to normal people without requiring them to be tech-savvy, what you want goes in complete opposition to that mission.

Apple has a lot to be criticized for but gatekeeper (and SIP) isn't that.

People like and need the apple sandbox. Others need an unlocked *nix machines

Otherwise, you have banks and MAFIAA and others off-loading their own security and compliance costs to users by flat out discriminating based on the status of the sandbox.

I've never ended up with undesired software on my system except for under two circumstances: either (a) it's installed by the OS vendor, or (b) some proprietary indie software I used got bought by a shady company who now wants to spy on me and sell my data. Systems like Gatekeeper don't protect against either.

> Also, it’s just such a bad security precedent. This page describes the error you get as “the typical macOS Gatekeeper warning”, as though it were just another piece of corporate silliness, like clicking through a EULA.

It mostly is another piece of corporate silliness. For most people it rarely does something useful. But I agree; if you're courting normie users you should just pony up and get your code signed and notarized. Otherwise just tell people that if they don't already know what Gatekeeper is and understand the risks of bypassing it as well as how to do so, your software isn't for them.

Even though it's more troublesome to submit apps to App Store, it's one signal that the app is not a malware.

In AI conversations, people often forget that at the end of a day, an actual human needs to use your stuff.

Let’s not forget when Apple’s certificate server was down and suddenly you couldn’t launch apps on macOS, to say nothing of the abuse of user rights.

lol

I applaud that they didn't kowtow to Apple's attempt to exercise control over their app and extort money from them. Why should we accede to policies that are designed to exploit us developers?

We developers add the real value to a platform. Don't believe me? Look up on how popular Sailfish OS or Windows Mobile OS is and why they failed or struggle. Apple should be grateful to this developer that they seek to add value to their platform instead of trying to figure out money grubbing ways on how to control and exploit them. (Of course, ultimately it is the users of the platform who are exploited - all charges by Apple are ultimately bore by them when they purchase an app through the App Store).

It's just sad that whether you are a user or a developer, Apple Fanbois would rather (ignorantly) place Apple's interest over their own consumer rights.

You think notarizing an app is "placing Apple's interest over" our own?

Thus, notarization also acts as a way for Apple to spy on its user and determine what apps they run - both when you install from the App Store or when you install it from outside the App Store. The way the whole process works, open source softwares (which are popular and compete with Apple's own app and other paid apps but often cannot bear the unnecessary burden of jumping through Apple's hoops) are also tarnished with all the popups about security threats, thus discouraging their use amongst non-technical users. This is great for Apple ofcourse because they can't make money of free open source developers (unless of course, they use their code to make their own applications, which they have no qualms about).

Imagine this too - How would you like it if Apple allowed you to view websites in Safari (or other macOS browsers) only if they had an SSL certificate from Apple?

So it is a disingenuous argument that people here are being "stupid" for complaining about Notarization. It's Apple forcing itself as the middle-man here and then exploiting its developers and users that's the issue.

Do you not realize that spending money on other useful services makes it harder, not easier, to waste on dev fees?

If you really want to ban Gatekeeper you can. sudo spctl --master-disable

As the saying goes about being careful, measure twice and cut once.

It IS another piece of corporate silliness. Though silliness is an extremely charitable word for what it really is

Cheering on the loss of autonomy and control over our own computers under the guise of 'silliness' is disgusting

  API Error: 529
  {
    "type": "error",
    "error": {
      "type": "overloaded_error",
      "message": "Overloaded. https://docs.claude.com/en/api/errors"
    },
    "request_id": "..."
  }

So the fact that 1.82.7 and then 1.82.8 were released within an hour of each other was highly suspicious.

But I believe you can replace versions on both, nonetheless. It’s a multi step process, unpublish then publish again. But the net effect is the same.

https://pypi.org/help/#file-name-reuse

> PyPI does not allow for a filename to be reused, even once a project has been deleted and recreated...

> This ensures that a given distribution for a given release for a given project will always resolve to the same file, and cannot be surreptitiously changed one day by the projects maintainer or a malicious party (it can only be removed).

The redraw glitches you’re referring to are actually signs of what I consider to be a pretty major feature, a reason to use `claude` instead of `codex` or `opencode`: `claude` doesn’t use the alternate screen, whereas the other two do. Meaning that it uses the standard screen buffer, meaning that your chat history is in the terminal (or multiplexer) scrollback. I much prefer that, and I totally get why they’ve put so much effort into getting it to work well.

In that context handling SIGWINCH has some issues and trickiness. Well worth the tradeoff, imo.

You can run a codex instance on machine A and connect the TUI to it from machine B. The same open source core and protocol is shared between the Codex app, VS Code and Xcode.

on my m1, claude is noticeably slower when starting, but it feels ok after that.

The LLMs are super good at doing that translation, though. They can write those formats no problem.