Hello! I have used Alloy to model a real-life system and find a hole in it. I have answers for you, but I’m afraid that I’m going to start by asking another question, and possibly throw a bit of cold water on your ambitions:
Is your primary objective to find holes in SELinux, or is your objective to integrate an LLM with a theorem prover / SMT solver? If you try to do both at the same time, I think you will have a harder time than if you choose just one.
The Google DeepMind team did not try to find unknown holes in a large and complex project. Instead, they solved a geometry test with known answers. They threw a very large number of CPU-hours at the feat of solving the same geometry test that one very smart high schooler could solve in a few hours.
I think you may find that proving the consistency of SELinux is harder than passing a geometry test, and if you have fewer PhDs and less computing hardware than Google Deepmind, I do not recommend trying to solve a more difficult problem than Google DeepMind chose to solve.