upvote

points

by throwaway274481 days ago |
comments
upvoteby ks20481 days ago|
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.

reply
upvoteby jll291 days ago|
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.)

reply
upvoteby caminante1 days ago|
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.

reply
upvoteby throwaway274481 days 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.
reply
upvoteby roywiggins1 days ago|
parent|
[-]
It seems pretty clear when you follow the link?

https://juxt.github.io/allium/

reply
upvoteby Aurornis1 days ago|
prev|
next
[-]
> 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.

reply
upvoteby throwaway274481 days ago|
parent|
next
[-]
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!)
reply
upvoteby MBCook1 days 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.

reply
upvoteby zeristor7 hours ago|
parent|
prev|
[-]
[dead]
reply
upvoteby Qwuke1 days ago|
prev|
[-]
>It's not even clear if AI was used to find the bug

It's not even clear you read the article

reply
upvoteby throwaway274481 days 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.

reply
upvoteby caminante1 days 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.

reply
upvoteby wat100001 days ago|
parent|
next
[-]
That's the opposite of clear to me.
reply
upvoteby Spinnaker_1 days 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"

reply
upvoteby chrisjj1 days ago|
parent|
prev|
[-]
> distilling

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

reply