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!
cc @Alexa VanHattum and @Michael McLoughlin for upstreaming plans -- I know that they want to do this soon-ish
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