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.
> distilling
A.k.a. as fabricating. No wonder they chose to use "AI".
That's the opposite of clear to me.
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"