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.

▲

ks2048 8 hours ago | parent | next [-]

They have some spec language and here,

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.

▲

jll29 9 hours ago | parent | prev | next [-]

> 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-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.)

▲

caminante 9 hours ago | parent | prev | next [-]

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 7 hours ago | parent [-]

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 4 hours ago \| parent [-]
		It seems pretty clear when you follow the link? https://juxt.github.io/allium/

▲

Qwuke 9 hours ago | parent | prev | next [-]

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

It's not even clear you read the article

▲

throwaway27448 7 hours ago | parent | next [-]

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 9 hours ago | parent | prev [-]

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 8 hours ago | parent | next [-]

> distilling

A.k.a. as fabricating. No wonder they chose to use "AI".

▲

wat10000 7 hours ago | parent | prev [-]

That's the opposite of clear to me.

	▲	Spinnaker_ 4 hours ago \| parent [-]
		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"

▲

Aurornis 9 hours ago | parent | prev [-]

> 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 7 hours ago | parent [-]

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 6 hours ago \| parent [-]
		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.