Stream: cranelift

Topic: The new rule verifier


view this post on Zulip Bongjun Jang (Jan 04 2026 at 06:10):

Hi! I just found an interesting project arrival which seems like the next-gen of crocus.

The paper says it can verify stateful rules (traps, ...) and more, unlike crocus. So it can verify broader group of rules than crocus.

I want to use this tool for mid-end rules.
But it looks like there is only a demonstration for a codegen backend (aarch64, x64, ...).
And the paper states it verifies a instruction-selection backend.
Is this possible to use this tool only for mid-end ISLE rules?

Plus, I want to hear a plan to integrate project this into the upstream wasmtime/cranelift, if any, just like crocus.

Thanks!

Instruction-selection verifier for the Cranelift compiler. - mmcloughlin/arrival

view this post on Zulip Chris Fallin (Jan 05 2026 at 05:18):

cc @Alexa VanHattum and @Michael McLoughlin for upstreaming plans -- I know that they want to do this soon-ish

view this post on Zulip Alexa VanHattum (Jan 07 2026 at 20:33):

Yes, arrival also can be used for mid-end rules, though some of that work happened after the paper and some of the details (mostly for floating point) are work-in-progress.

We are working on upstreaming this spring! I will try and see if we can prioritize landing the non-floating point stuff first to have it available to you sooner. Feel free to DM me if you'd like to locally run it sooner and I can try and put together instructions beyond the artifact details


Last updated: Jan 09 2026 at 13:15 UTC