3 ms·

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 h

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 7mo 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 7mo 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 7mo 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 7mo ago
  [dead]
jll29 7mo 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 7mo ago
>It's not even clear if AI was used to find the bug It's not even clear you read the article
- caminante 7mo 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 7mo ago
    > distilling A.k.a. as fabricating. No wonder they chose to use "AI".
  - wat10000 7mo ago
    That's the opposite of clear to me.
    - Spinnaker_ 7mo 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 7mo ago
        This is the original article text. It just looks like users skimmed and then flamed the author.
- throwaway27448 7mo 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 7mo 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 7mo 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 7mo ago
    It seems pretty clear when you follow the link? https://juxt.github.io/allium/ https://juxt.github.io/allium/
ks2048 7mo 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.

Aurornis 7mo 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 7mo 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 7mo 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 7mo ago
[dead]

jll29 7mo 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 7mo ago

>It's not even clear if AI was used to find the bug It's not even clear you read the article

caminante 7mo 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 7mo ago
  > distilling A.k.a. as fabricating. No wonder they chose to use "AI".
- wat10000 7mo ago
  That's the opposite of clear to me.
  - Spinnaker_ 7mo 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 7mo ago
      This is the original article text. It just looks like users skimmed and then flamed the author.
throwaway27448 7mo 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 7mo 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 7mo 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 7mo ago
  It seems pretty clear when you follow the link? https://juxt.github.io/allium/ https://juxt.github.io/allium/

ks2048 7mo 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.