skybrian's recent activity

  1. Comment on LLMs are making formal software verification feasible at a much larger scale in ~comp

    skybrian
    Link
    From the article: [...] [...] [...] [...] [...] [...] [...]

    From the article:

    For this project, we started with fuzz tests. In these tests, developers write an entry point2 into their code that takes inputs, such that any input that causes a crash is a bug the authors care about. Then the fuzzer, a testing engine, generates enormous numbers of semirandom and mutated inputs at the entry point to try to find a bug (visualized in Figure 1). The longer a fuzzer runs, the more bugs it can find. But this is inherently a brute-force process, with no guarantee of exercising every possible code path, regardless of how many inputs you try.

    [...]

    To find all the bugs that would’ve been surfaced by a fuzz test, we turned the fuzz test into a spec defined over the compiled RISC-V instructions. The spec says that the fuzz test won’t crash for any input less than 64 MB.3 If Claude can prove this spec, the fuzz test on RISC-V becomes superfluous: fuzzing that entry point will never find any bugs.

    We did this for hundreds of projects in Google’s OSS-Fuzz initiative, which provides continuous fuzz testing for qualifying open-source projects. OSS-Fuzz contains thousands of developer-authored entry points that look for broken code properties by crashing (for example, on a failed assertion). OSS-Fuzz automatically instruments C and C++ programs with AddressSanitizer4 (ASan), causing them to crash whenever memory is accessed improperly (which is a leading cause of software vulnerabilities). Broad-spectrum specifications like memory safety apply to almost all software.

    [...]

    Over the span of a few weeks, Claude successfully patched the bugs it found and then proved that there are no crashes on any input (up to 64 MB) for 239 entry points across 123 different OSS-Fuzz libraries. These proofs operate on the compiled RISC-V instructions (i.e., executable binaries), and they comprise about 180 million lines of Rocq, with a typical proof running to about 600,000 lines to provide security guarantees on binaries with a median length of 18,000 RISC-V instructions. These proofs are built by translating the RISC-V assembly code to a mathematical model using Theorem’s RISC-V instruction and Linux process semantics. This means these proofs currently assume that the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU using Linux OS. Expanding the scope of these proofs is well within reach, as it would involve standardizing semantics for more assembly architectures and other operating system processes. See an expert’s take on the proofs Claude wrote.

    [...]

    This doesn’t mean these libraries contain no bugs. Instead, it means that any remaining bugs either are to be found within the artifacts listed above or are outside the scope of Claude’s proof. Hardening those still-possibly-buggy trusted components (Rocq, RISC-V, and Linux semantics) is not insignificant, but it’s a far more tractable task than debugging every line of code the scaled-out proofs cover—especially as this approach can secure an arbitrary number of projects without increasing the size of the trusted components.

    [...]

    Many of the bugs we found are ones that a fuzzer would be unlikely to ever find. Fuzzers mutate small inputs, typically capped at 1 MB, and typically rely on code coverage to guide them toward bugs. While proving an entry point in one library, Claude found a counter underflow in its copy of a decompressor that led to an out-of-bounds write, but only on inputs of around 20 MB that had one rare, specific layout. Other bugs include an out-of-bounds read in an image decoder that needed a 64 MB input and over 2 GB of memory, an out-of-bounds read in another library that needed a particular sequence of calls across two handles to the same file, and a rediscovery of CVE-2026-56132 in libexpat, which needed deeply nested input. Claude also found logic bugs that never crash at all. While proving that one library was memory-safe, for example, it noticed that a feature for restricting which files an application can load isn’t always enforced.

    [...]

    Proving that a fuzz test has no more crashes to find is more significant than it sounds. It’s common for fuzz tests in real-world code to test for violations of meaningful high-level properties, such as encode-decode roundtripping, idempotence, algebraic laws, differential testing, self-consistency, or equivalence to reference implementations. For example, a fuzz test for the LZO compression algorithm asserts that if you compress an input, then decompress it, the result is the same as the original. If the property does not hold, the program crashes—so proving the test never crashes is equivalent to proving the property itself.

    This can also occur even when the properties are not directly specified by the developer. For example, in order for Claude to complete its OSS-Fuzz proof for cpp-httplib, it was necessary to rule out the possibility of a stack overflow due to too much recursion in the std::set destructor. This recursion depth is bounded by the maximum depth of a tree, so Claude had to prove (on machine code!) that libc++’s red-black tree rebalancing algorithm is correctly optimized to keep the tree’s depth logarithmically bounded.

    [...]

    In another experiment, we asked Claude to develop an interpreter for a large subset of Python in Rust, and to prove (using Verus, a verification tool for Rust) that it adheres to the CPython semantics outlined in an academic paper. We then measured the adherence to CPython’s behavior empirically, running over 1.7 million randomly generated Python programs, finding identical behavior with CPython in 99.95% of tests, with remaining test differences as unsurprising known corner cases.

    We also found issues in several widely used and critical applications via formal verification attempts of simple security properties. In one of them, we discovered a previously unknown logic bug that had been latent for more than a decade. During an effort to verify a widely used PDF reader, we found as many security bugs in one week as are typically reported in a year.

    [...]

    This reusability of proofs is how Mathlib, a shared library of formal mathematics in Lean, grew to nearly 300,000 theorems submitted by over 700 contributors: each new proof builds on the existing body of work. We accumulated a similar body of proofs in the course of our OSS-Fuzz effort, some of which we’re including in our release (we are not releasing proofs that may reveal an unpatched bug in the open-source software).

    1 vote

  3. Comment on Offbeat Fridays – The thread where offbeat headlines become front page news in ~news

    skybrian
    Link
    Meet the Guy Who Excavated O’Hare’s 50-Ton Boulder From the article: [...] [...] [...] [...]

    Meet the Guy Who Excavated O’Hare’s 50-Ton Boulder

    From the article:

    Ron Pitelka has an idea for what to name the 50-ton prehistoric boulder that was unearthed this summer at O’Hare Airport.

    “I would probably call it ‘Geo,’” Pitelka said. “It might not be funny, but it’s a little more appropriate.”

    [...]

    In all of the 23 years he’s been operating excavators — so, half his life — “I’ve never seen a boulder this big come out of the ground. It’s pretty damned rare,” Pitelka, who lives in Homer Glen, told WTTW News. “I was like a kid on Christmas.”

    [...]

    Pitelka’s colleague, Matt Tracy, attempted to budge the object with his bulldozer. It didn’t move. Pitelka tried to hook it and the Cat 352 balked. Eventually, with the combined force of the bulldozer pushing and the excavator pulling, they got the boulder out of the ground.

    [...]

    Over the years, Pitelka has rescued some of these rocks and deposited them at his mom’s five-acre property, including a large hunk of limestone that, when he dumped it out of his truck, split in half to reveal a perfect trilobite fossil, convex on one side and a matching imprint on the other.

    “I’m always looking for stuff like that,” he said. “When I go on vacation, I always bring a rock back.”

    [...]

    Knowing that the massive find at O’Hare could easily be 300 to 400 million years old, Pitelka asked the construction superintendent to fight for the behemoth’s preservation. He hoped maybe it could be embedded in the basin’s embankment, where he could view it via Google earth.

    It was only this week, when the airport announced the naming contest for the rock, that Pitelka learned the boulder had been saved and was destined for greater things.

    “I was so excited to hear that the right people got involved,” he said. “I’m absolutely ecstatic it’s going to be on display. For me, as an (excavator) who loves boulders, it’s the coolest thing that people understand its historical significance and appreciate it.”

    2 votes

  4. Comment on US State Department unveils plan to only promote Donald Trump supporters in ~society

    skybrian
    Link Parent
    No, the idea that it would happen that way, where we would wake up surprised by the election results that are obviously a fraud, is still magical thinking. Voting is very decentralized. Their...

    No, the idea that it would happen that way, where we would wake up surprised by the election results that are obviously a fraud, is still magical thinking. Voting is very decentralized. Their attempts would take time, and would be reported on. They have been reported on.

    1 vote

  5. Comment on US State Department unveils plan to only promote Donald Trump supporters in ~society

    skybrian
    (edited )
    Link Parent
    Yes, of course it's a serious concern, as an immigration issue and a civil rights issue, but it's not going to affect the elections. (Other than as a campaign issue.)

    Yes, of course it's a serious concern, as an immigration issue and a civil rights issue, but it's not going to affect the elections. (Other than as a campaign issue.)

  6. Comment on US State Department unveils plan to only promote Donald Trump supporters in ~society

    skybrian
    Link Parent
    Yes, they will keep trying, but they're still not Lex Luthor. Overturning a Supreme Court ruling isn't a matter of getting more lawyers involved. A prediction with a "magic happens here" step in...

    Yes, they will keep trying, but they're still not Lex Luthor. Overturning a Supreme Court ruling isn't a matter of getting more lawyers involved. A prediction with a "magic happens here" step in the middle isn't very credible, and by spreading FUD you're acting as the Trump administration's dupe. They can't stop enough people from voting to matter, so they're going to try to scare them away instead. Why help?

    3 votes

  7. Comment on US State Department unveils plan to only promote Donald Trump supporters in ~society

    skybrian
    Link Parent
    Certainly the Trump administration has tried in many ways. But you are not more clear. Did not happen! The Supreme Court ruled against them. They're still trying, but they keep failing. And even...

    Certainly the Trump administration has tried in many ways. But you are not more clear.

    Revoking birthright citizenship

    Did not happen! The Supreme Court ruled against them. They're still trying, but they keep failing.

    And even if it did happen, it wouldn't effect the elections for long after Trump is gone, because babies don't vote!

    So why bring it up? Why are you muddying the waters? Why are you trying to make Trump seem ten feet tall? Whose side are you really on?

    4 votes

  8. Comment on US State Department unveils plan to only promote Donald Trump supporters in ~society

    skybrian
    Link Parent
    It is, though. This is terrible, but it's unlikely to affect the elections. Please vote. And don't discourage people from voting! That's just making it worse.

    "You'll never have to vote again" wasn't hyperbole.

    It is, though. This is terrible, but it's unlikely to affect the elections. Please vote. And don't discourage people from voting! That's just making it worse.

    7 votes

  9. Comment on Non-queer men of Tildes: PLEASE consider before commenting on ~life.women and ~lgbt without careful consideration. We are losing members over this issue. in ~tildes

    skybrian
    (edited )
    Link Parent
    If one person experiences it, it's a real issue. But there is a difference in logic between #MeToo and #YesAll tags. #YesAll tags are making a much stronger claim. Not just that you experienced...

    If one person experiences it, it's a real issue. But there is a difference in logic between #MeToo and #YesAll tags. #YesAll tags are making a much stronger claim. Not just that you experienced it, or that the experience is common, but that "everyone" experiences it. This is not just about yourself. It's denying the lived experiences of strangers that you have no right to speak for. It's denying that the world is a diverse place and people have different experiences. It's saying that no, actually, things are the same everywhere. Who has the right to make such a claim from personal experience?

    As a matter of logic, saying that "everyone" experiences something actually is refuted by someone saying, "well I don't see it." #YesAll a very strong claim, often easily disproved.

    Though of course, people are not computer programs and often we say things that aren't meant literally. The meaning of a term in context could be something else entirely.

    A charitable way to understand #YesAll is to assume that it's not what they really meant. But the term itself argues for being taken literally. It's effectively saying "I meant what I said."

    So, if you don't want that meaning, maybe avoid using "YesAll" hashtags?

    10 votes

  10. Comment on eMudhra intermediate CA compromise in ~tech

  11. Comment on PHP warns it plans to release two emergency patches imminently in ~comp

    skybrian
    Link Parent
    Here is Calif’s page on the bug:

    Here is Calif’s page on the bug:

    No special harness, or access to models that weren't generally available to everyone were used in the initial bug discovery. I focused on something I had a background in, knew its vulnerability history well, and held a theory that specific bugs lurk within the codebase. This shows that "know your target" is still as applicable as ever, even in the LLM dominated VR age. No model is simply capable of unearthing "all bugs" with simple prompts. At least for now.

    There are some practical research implications here. LLMs may have ingested public historical vuln data, but in their default variant analysis tends to move from the newest and most prominent bugs toward nearby older code. They do not reliably begin with obscure twenty-year-old exploitation primitives. Keeping your own mental catalog of a target's vulnerability history lets you prompt that direction explicitly.

    5 votes

  12. Comment on Non-queer men of Tildes: PLEASE consider before commenting on ~life.women and ~lgbt without careful consideration. We are losing members over this issue. in ~tildes

  13. Comment on PHP warns it plans to release two emergency patches imminently in ~comp

    skybrian
    Link
    And yep, these bugs were found via AI. From the Wiz blog: ... ... And if they didn't find it, apparently someone else would have? From OpenAI's blog: (Calif is apparently a security firm.)

    And yep, these bugs were found via AI.

    From the Wiz blog:

    In this post, we explain how frontier AI helped us find and fix vulnerabilities that had remained hidden in the PHP codebase for more than a decade. The issues described below all stem from key architecture decisions, some made over a decade ago, and were grouped under two CVEs, with severity reaching CVSS 9.2. The work grew into a cross-industry effort to protect customers, find variants, deploy detections and mitigations, and verify a patch in time for coordinated disclosure.

    ...

    We believe PHP2Shell could mark a similar turning point for the AI era, illustrating how AI can change the practical exploitability of longstanding vulnerabilities. Building the exploit required chaining multiple flaws and adapting to each target’s memory layout through repeated testing and debugging. Frontier models were critical to making this process practical, enabling us to develop and adapt working exploits across multiple applications in hours. As the time and expertise required for this work decrease, complexity may no longer provide a meaningful barrier, changing how we define what is vulnerable in practice.

    ...

    We used Wiz Atlas, Gemini 4 Argon and GPT-5.6 Sol throughout this research. Notably, Gemini 4 Argon made an invaluable contribution to finding the vulnerability, exploit development, attack detection, and validation of the patch.

    And if they didn't find it, apparently someone else would have? From OpenAI's blog:

    Calif identified a critical flaw using GPT‑5.6 Sol as part of our Patch the Planet initiative, with Wiz also independently discovering and reporting both vulnerabilities

    (Calif is apparently a security firm.)

    2 votes

  14. Comment on Non-queer men of Tildes: PLEASE consider before commenting on ~life.women and ~lgbt without careful consideration. We are losing members over this issue. in ~tildes

    skybrian
    Link Parent
    I doubt anyone post links here because they they think they’re bait. They post them because they agree with them or at least think they’re interesting. But writing style can be contagious and...

    I doubt anyone post links here because they they think they’re bait. They post them because they agree with them or at least think they’re interesting. But writing style can be contagious and “interesting” links are sometimes originally from influencers or people writing in a similar style, because it seems catchy. It might not seem objectionable when you’re on the same side.

    8 votes

  15. Comment on Non-queer men of Tildes: PLEASE consider before commenting on ~life.women and ~lgbt without careful consideration. We are losing members over this issue. in ~tildes

    skybrian
    Link Parent
    It’s true that we are responsible for our own posts and our own replies. But also true that we are asked to try to think about how others might respond. When starting a topic, there is this...

    It’s true that we are responsible for our own posts and our own replies. But also true that we are asked to try to think about how others might respond. When starting a topic, there is this boilerplate:

    Please post topics that are interesting, informative, or have the potential to start a good discussion.

    What would a good discussion look like? Sometimes you can post something along with a link that tries to head things in a good direction.

    It doesn’t always work and it can be taken too far so you don’t post at all. I think there’s a middle ground?

    There’s also a common impulse to try to influence what other people post. That’s what this topic about, right? It’s yet another discussion of what should be okay to post. We have no control over what other people do, but sometimes we try to influence them.

    5 votes

  16. Comment on Non-queer men of Tildes: PLEASE consider before commenting on ~life.women and ~lgbt without careful consideration. We are losing members over this issue. in ~tildes

    skybrian
    Link
    A few points: First, there’s something liberating about saying you’re out of touch. Getting into a situation where you’re claiming to be an expert in gender relations everywhere in the world is...

    A few points:

    First, there’s something liberating about saying you’re out of touch. Getting into a situation where you’re claiming to be an expert in gender relations everywhere in the world is kind of ridiculous. For example, I have read a few articles about gender relations in South Korea and it seems rather weird and bad, but I won’t claim to really understand it. I’ve never been there!

    Second, baiting people is extremely common tactic to get clicks and/or start an argument. Sometimes people share stuff like that, perhaps even with the original click-bait title. That doesn’t necessarily mean the person who posted the link meant to start an argument, but it often does have that effect. With experience, we can learn not to engage, or to do it in a more thoughtful way.

    Third, #YesAllMen (the tag) is definitely going to act as bait, intentional or not. It’s vague, so it can have better or worse interpretations, but the person posting it can be seen as claiming they know something about “all men,” which can be seen as telling strangers that you know better than them about their own lived experiences. So it’s natural for people to object to that and can easily become heated. On the other hand, it’s obviously hyperbolic (cultures are not all the same and nobody could possibly know about all men in every culture). If it’s not taken literally, what meaning remains? Perhaps it’s a flag to rally around?

    Since I’m attempting to avoid taking the bait myself, I won’t look any deeper. What can we conclude from this? Maybe let’s try to avoid posting bait and try to avoid responding to it, or at least avoid responding to it as bait.

    16 votes

  17. Comment on Anthropic logged net loss of over $80 billion in first half of 2026 in ~tech

    skybrian
    Link Parent
    The investors that own convertible notes are likely fine in almost any circumstances. If things don't go well, the risk is like owning a bond. The debt is owed by Anthropic to the investors. The...

    The investors that own convertible notes are likely fine in almost any circumstances. If things don't go well, the risk is like owning a bond. The debt is owed by Anthropic to the investors. The only way they wouldn't get their money back is if Anthropic went bankrupt.

    Why did the investors get such good terms? If it's like other startups, it's because they got in early, before anyone knew how big Anthropic would be. They gave Anthropic money back when it needed money and there was a risk it wouldn't make it. But at this point, for all early investors in Anthropic, it's just a matter of how great an investment it will turn out to be, because they got in at a very low price.

    (For investors buying during the IPO, the risks are different, because that's a much higher price.)

    4 votes

  18. Comment on Non-queer men of Tildes: PLEASE consider before commenting on ~life.women and ~lgbt without careful consideration. We are losing members over this issue. in ~tildes

    skybrian
    (edited )
    Link Parent
    By “not a well agreed concept,” do you mean specifically on Tildes or in general? Because I do think such places exist, such as private chats. A Tildes group isn’t a private chat, though. Tildes...

    By “not a well agreed concept,” do you mean specifically on Tildes or in general? Because I do think such places exist, such as private chats. A Tildes group isn’t a private chat, though.

    Tildes is something of a bubble, though, in a good way. It’s invite-only for good reason. It’s not as much of a bubble as sometimes people hope.

    5 votes

  19. Comment on I teach at a business school. It’s time to shut them down. (gifted link) in ~life

    skybrian
    Link Parent
    Okay, there is a link that goes to the Bloomberg article with the title “Academics question ESG studies…”. I can’t read it, though.

    Okay, there is a link that goes to the Bloomberg article with the title “Academics question ESG studies…”. I can’t read it, though.

  20. Comment on AI proved the Quasi-Riemann hypothesis. What happens Now? in ~science

    skybrian
    Link Parent
    Well, math is deterministic. There is a sense in which we could, in principle, calculate whether any number is prime. We already do this for numbers that aren’t extremely large. But being able to...

    Well, math is deterministic. There is a sense in which we could, in principle, calculate whether any number is prime. We already do this for numbers that aren’t extremely large.

    But being able to calculate something in principle doesn’t mean we can do it in practice for all numbers. There will always be numbers that are too big to manipulate using any computer we could possibly build.

    Theoretical math is about what we can say about numbers that are too large to calculate. Testing a few trillion numbers tells us something, but you never know if there will be a counterexample that’s just beyond the numbers we tested. This is why it’s done by proving theorems rather than doing calculations.

    4 votes