3 ms·

Has someone verified this was an actual bug? One of AI’s strengths is definitely exploration, f.e. in finding bugs, but it still has a high false positive rate

by jwpapi 6mo ago

Has someone verified this was an actual bug? One of AI’s strengths is definitely exploration, f.e. in finding bugs, but it still has a high false positive rate. Depending on context that matters or it wont. Also one has to be aware that there are a lot of bugs that AI won’t find but humans would I don’t have the expertise to verify this bug actually happened, but I’m curious.

throwaway27448 6mo ago
It's not even clear if AI was used to find the bug: they mention modeling the software with an "ai native" language, whatever that means. What is not clear is how they found themselves modeling the gyros software of the apollo code to begin with. But, I do think their explanation of the lock acquisition and the failure scenario is quite clear and compelling.
- Aurornis 6mo ago
  > It's not even clear if AI was used to find the bug The intro says “We used Claude and Allium”. Allium looks like a tool they’ve built for Claude. So the article is about how they used their AI tooling and workflow to find the bug.
  - throwaway27448 6mo ago
    The article does not explain anything about how they used AI—it just has some relation with the behavioral model a human seems to have written (and an AI does not seem necessary to use!)
    - MBCook 6mo ago
      Sure it does. They used their AI tool to extract the rules for the Apollo guidance system based on the source code. Then they used Claude to check if all paths followed those rules.
  - zeristor 6mo ago
    [dead]
- jll29 6mo ago
  > It's not even clear if AI was used to find the bug: they mention modeling the software with an "ai native" language, whatever that means. Could the "AI native language" they used be Apache Drools? The "when" syntax reminded me of it... https://kie.apache.org/docs/10.0.x/drools/drools/language-reference-traditional/index.html https://kie.apache.org/docs/10.0.x/drools/drools/language-re... (Apache Drools is an open source rule language and interpreter to declaratively formulate and execute rule-based specifications; it easily integrates with Java code.)
- Qwuke 6mo ago
  >It's not even clear if AI was used to find the bug It's not even clear you read the article
  - caminante 6mo ago
    Even worse, the other child comments are speculating (and didn't RTFA either) when the answer is clear in the article. > We found this defect by distilling a behavioural specification of the IMU subsystem using Allium, an AI-native behavioural specification language.
    - chrisjj 6mo ago
      > distilling A.k.a. as fabricating. No wonder they chose to use "AI".
    - wat10000 6mo ago
      That's the opposite of clear to me.
      - Spinnaker_ 6mo ago
        Has the article been updated? 2nd paragraph starts with: "We used Claude and Allium" And later on: "With that obligation written down, Claude traced every path that runs after gyros_busy is set to true"
        Qwuke 6mo ago
        This is the original article text. It just looks like users skimmed and then flamed the author.
  - throwaway27448 6mo ago
    Where do you think my confusion came from? All it says is that ai assists in resolving the gyroscope lock path, not why they decided to model the gyroscope lock path to begin with. Please, keep your offensive comments to yourself when a clarifying comment might have sufficed.
- caminante 6mo ago
  How did you pick out AI native and miss the rest of the SAME sentence? > We found this defect by distilling a behavioural specification of the IMU subsystem using Allium, an AI-native behavioural specification language.
  - throwaway27448 6mo ago
    That does not answer my confusion, especially when static analysis could reveal the same conclusion with that language. It's not clear what role ai played at all.
    - roywiggins 6mo ago
      It seems pretty clear when you follow the link? https://juxt.github.io/allium/ https://juxt.github.io/allium/
- ks2048 6mo ago
  They have some spec language and here, https://github.com/juxt/Apollo-11/tree/master/specs https://github.com/juxt/Apollo-11/tree/master/specs have many thousands of lines of code in it. Anyways, it seems it would take a dedicated professional serious work to understand if this bug is real. And considering this looks like an Ad for their business, I would be skeptical.

by jwpapi 6mo ago

throwaway27448 6mo ago

It's not even clear if AI was used to find the bug: they mention modeling the software with an "ai native" language, whatever that means. What is not clear is how they found themselves modeling the gyros software of the apollo code to begin with. But, I do think their explanation of the lock acquisition and the failure scenario is quite clear and compelling.

Aurornis 6mo ago
> It's not even clear if AI was used to find the bug The intro says “We used Claude and Allium”. Allium looks like a tool they’ve built for Claude. So the article is about how they used their AI tooling and workflow to find the bug.
- throwaway27448 6mo ago
  The article does not explain anything about how they used AI—it just has some relation with the behavioral model a human seems to have written (and an AI does not seem necessary to use!)
  - MBCook 6mo ago
    Sure it does. They used their AI tool to extract the rules for the Apollo guidance system based on the source code. Then they used Claude to check if all paths followed those rules.
- zeristor 6mo ago
  [dead]
jll29 6mo ago
> It's not even clear if AI was used to find the bug: they mention modeling the software with an "ai native" language, whatever that means. Could the "AI native language" they used be Apache Drools? The "when" syntax reminded me of it... https://kie.apache.org/docs/10.0.x/drools/drools/language-reference-traditional/index.html https://kie.apache.org/docs/10.0.x/drools/drools/language-re... (Apache Drools is an open source rule language and interpreter to declaratively formulate and execute rule-based specifications; it easily integrates with Java code.)
Qwuke 6mo ago
>It's not even clear if AI was used to find the bug It's not even clear you read the article
- caminante 6mo ago
  Even worse, the other child comments are speculating (and didn't RTFA either) when the answer is clear in the article. > We found this defect by distilling a behavioural specification of the IMU subsystem using Allium, an AI-native behavioural specification language.
  - chrisjj 6mo ago
    > distilling A.k.a. as fabricating. No wonder they chose to use "AI".
  - wat10000 6mo ago
    That's the opposite of clear to me.
    - Spinnaker_ 6mo ago
      Has the article been updated? 2nd paragraph starts with: "We used Claude and Allium" And later on: "With that obligation written down, Claude traced every path that runs after gyros_busy is set to true"
      - Qwuke 6mo ago
        This is the original article text. It just looks like users skimmed and then flamed the author.
- throwaway27448 6mo ago
  Where do you think my confusion came from? All it says is that ai assists in resolving the gyroscope lock path, not why they decided to model the gyroscope lock path to begin with. Please, keep your offensive comments to yourself when a clarifying comment might have sufficed.
caminante 6mo ago
How did you pick out AI native and miss the rest of the SAME sentence? > We found this defect by distilling a behavioural specification of the IMU subsystem using Allium, an AI-native behavioural specification language.
- throwaway27448 6mo ago
  That does not answer my confusion, especially when static analysis could reveal the same conclusion with that language. It's not clear what role ai played at all.
  - roywiggins 6mo ago
    It seems pretty clear when you follow the link? https://juxt.github.io/allium/ https://juxt.github.io/allium/
ks2048 6mo ago
They have some spec language and here, https://github.com/juxt/Apollo-11/tree/master/specs https://github.com/juxt/Apollo-11/tree/master/specs have many thousands of lines of code in it. Anyways, it seems it would take a dedicated professional serious work to understand if this bug is real. And considering this looks like an Ad for their business, I would be skeptical.