RFC: Forming a Working Group on Formal Specification for LLVM

LLVM Project
1

Hi LLVM Community,

We propose forming a new working group to focus on formal specification for LLVM IR.

We have briefly discussed this at an impromptu roundtable (LLVM Developer's Meeting 2025: Roundtable on formal sematics for LLVM (notes) - Google Docs) at the US LLVM Developer’s Meeting this year and additionally offline with a group of people interested in this topic.

The goal is to bring together experts from multiple programming language communities and academia to dive into more detailed discussions and coordinate efforts from open source contributors and research groups on the topic of LLVM’s formal specification and it’s semantic model.

Logistics

Meetings: We tentatively plan to have a first kick off meeting next week (exact time and day to follow) and then continue next year, starting mid January 2026, with 1h bi-weekly syncs. We are doing our best to accommodate a wide range of timezones (GMT-8h to GMT+1h) and other scheduling restrictions.

Communication: We plan to keep meeting notes that can be read offline by interested parties. As a forum for additional discussions, we’re looking to initially use discourse, email and impromptu syncs where necessary to make progress. We’re looking into also having a Discord channel.

Participants

We encourage anyone interested to participate in this group. The meetings will be public, as well as the notes doc.

Sharing also the group of folks who we’ve discussed with in more depth on the first iteration of this working group.

Alina Sbirlea - Google
Burak Emir - Google
Dmytro Hrybenko - Google
Chandler Carruth - Google
James Y Knight - Google
John McCall - Apple
John Regehr - University of Utah
Kayvan Memarian - University of Cambridge
Nikita Popov - Red Hat
Nuno Lopes - University of Lisbon
Peter Sewell - University of Cambridge
Ralf Jung - ETH Zürich
Richard Smith - Google
Steve Zdancewic - Pennsylvania State University
Tobias Grosser - University of Cambridge

Initial write-ups

Referencing the following for additional background and to guide the initial discussions:

* https://hackmd.io/@nikic/SJBt4mFCll

* LLVM IR semantic changes for safety

Looking forward to hearing your thoughts on this!

19 Likes
LLVM Weekly - #623, December 8th 2025
2

Hello,

We’re planning a kick off meeting next week, Monday, December 8th at 8:30am PT / 11:30am ET / 4:30pm GMT / 5:30pm GMT+1.
For next week, the meet link is: meet.google.com/rqd-yggb-tux. I added this to the LLVM Calendar.

We’ll pick it back up in January with the first 2026 meeting on Monday, January 12th at 8:30am PT / 11:30am ET / 4:30pm GMT / 5:30pm GMT+1.
This will be a recurring meeting using: meet.google.com/yfe-xbnv-acb. I added this to the LLVM Calendar as well.

Thank you,
Alina

7 Likes
3

We will have the first meeting of 2026 next Monday, January 12th at 8:30am PT / 11:30am ET / 4:30pm GMT / 5:30pm GMT+1., as previously scheduled.
The meeting is shared with the LLVM calendar for easy access (calendar@llvm.org).

The notes doc has a list of pre-reading material on the byte type which I would like to discuss during this meeting.

If you would like to bring up additional discussion topics for either next or subsequent meetings, please add these to the notes.

2 Likes
4

Beautiful :heart_eyes: Completely approve of this group :smiley:

5

@alina I see that there is a one-off meeting scheduled for this Friday. Is that taking place? It seems a bit weird given that there’s another meeting the following Monday.

6

There won’t be a meeting on Friday, the next sync will be the regular Monday one.

1 Like