CFP: RustINDIA Conference 2026

A number of Rust projects rely on the SIMD intrinsics provided by core::arch for performance. This includes libraries like hashbrown that are used in HashMap, as well as third-party cryptographic libraries like libcrux and Dalek that are used in mainstream software projects. However, the SIMD intrinsics in Rust lack documentation and are easy to misuse, and so even the best Rust programmers need to wade through Intel or Arm assembly documentation to understand the functional behaviour of these intrinsics.

This talk discusses the development of a Rust library which provides models for these intrinsics written in pure Rust, alongside the development of tests that ensure these models match the functional behaviour of the Rust intrinsics. Through the development of this Rust library, we were able to build models of 384 x86 intrinsics, and 181 aarch64 intrinsics. Furthermore, I discuss how this work led to the discovery of bugs in the Rust core with the implementation of these intrinsics. This was accepted as a solution a challenge worth 20,000 dollars put forth by AWS.

Hopefully this session is beneficial for people interested within the internal details of the Rust compiler, along with those interested in proving correctness of a variety of Rust programs.

I am Aniket Mishra, a BTech 3rd Year student at IIT Gandhinagar. This talk is based off of work done during my internship with CRYSPEN, a startup that focusses on proving the correctness of Rust Programs, particularly those involving cryptography.