The use of Alloy and LLM's

Hi! This is exactly what I’m going to be working on starting in a week – I’ve enrolled at The Recurse Center for a 6-week (March 25 - May 3) professional sabbatical. I have lots of ideas, but generally I’m playing in this space of Formal Models integrated into day-to-day dev settings, bridged by LLM. I generally work in Rails applications, and have good vibes with Alloy, so I’m starting with Alloy+LLM+Rails.

Pre-gaming in research a bit, this is very aligned with the work that Sullivan is doing at SCOPE Lab, and I’ve run into other Rails+Alloy projects too, such as Near’s earlier work on Rubicon, a (defunct) ruby RSpec DSL that integrates Alloy into working test suites.

I’m imagining taking a working codebase (say a Rails app), extracting one or more Alloy models using LLM stuff, maybe also taking some direction of what we want to explore / prove / disprove, and then generate back unit tests (say Rspec tests) that pass/fail as expected. In Rails this might be focused on the models, API interactions, existing test functionality, etc – so I’m hoping that there is enough consistent structure there for the cleverness of Hans to turn into something practical. Maybe something that can get into the CI/CD pipeline. Dunno.

One of my co-workers suggested focusing on cancan access control as an even more focused subset, which makes sense, and there are likely other areas. But I want to swing for the stars.

I welcome ideas!!! Since I’ll be working on this more or less full time, I’m also up for direct collaboration or brainstorming on zoom and whatnot. I’ll be in Brooklyn for the duration and would be happy to buy someone an IRL coffee if they wanna talk Alloy+LLM+Rails or some overlap therein :slight_smile:

1 Like