# Using Alloy to verify SELinux policies: Seeking advice on neurosymbolic approaches **URL:** \ **Category:** Questions\ **Created:** [August 26, 2024, 3:22pm UTC](https://alloytools.discourse.group/t/using-alloy-to-verify-selinux-policies-seeking-advice-on-neurosymbolic-approaches/481 "2024-08-26T15:22:02Z")\ **Posts on this page:** 1\ **Showing post:** 2
**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\ **Post date:** [August 27, 2024, 10:57pm UTC](https://alloytools.discourse.group/t/using-alloy-to-verify-selinux-policies-seeking-advice-on-neurosymbolic-approaches/481/2 "2024-08-27T22:57:09Z")
Hello! [I have used Alloy to model a real-life system and find a hole in it](https://alloytools.discourse.group/t/a-real-world-success-story/443). 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. --- _[View the full topic](https://alloytools.discourse.group/t/using-alloy-to-verify-selinux-policies-seeking-advice-on-neurosymbolic-approaches/481)._