What we have learned at OpenShell applying formal methods to control AI agents
alexwatson405
32 points
11 comments
September 15, 2026
Related Discussions
Found 5 related stories in 81.1ms across 6,718 title embeddings via pgvector HNSW
- Show HN: Open-source playground to red-team AI agents against public prompts zachdotai · 13 pts · August 09, 2026 · 55% similar
- Show HN: Talos – An AI agent with a permission kernel between model and shell kurdman_007 · 14 pts · August 28, 2026 · 54% similar
- OpenAI’s Navier-Stokes release included a Lean 4 formal proof ibobev · 153 pts · September 10, 2026 · 54% similar
- Terminal-Bench-Science: Evaluating AI agents on scientific research workflows matt_d · 61 pts · August 28, 2026 · 53% similar
- Discovery of a new OpenAI agent message board moultano · 1600 pts · September 04, 2026 · 53% similar
Discussion Highlights (5 comments)
agentdev001
Absolutely love openshell as a solution, I really hope Kube support moves out of experimental some time in the near future. Cool solution here- to a problem that I imagine is probably impossible to get 100% Looking forward to 0.1.0 release :)
xnx
For a moment I thought agentic AI had really spread to every project, but this is not related to the open-source Windows Start menu replacement: https://github.com/Open-Shell/Open-Shell-Menu
zaphar
I don't really feel like permissions is the hard bit here. The hard bit is that for an agent to do any kind of useful work it needs access to a lot of stuff. Further, the stuff it needs access to probably has vulnerabilities the agent can do. We have not exactly designed our environments for a use case like this. I've gone through the sandboxing exercise for an agent and by the time I had given it enough permissions to do anything useful my sandbox looked like swiss cheese.
philipwhiuk
> Back in the 2016 timeframe, members of our team were working at AWS and faced a similar challenge. Given all of the awesome complexity of AWS IAM policies, AWS S3 storage policies, historical version support- can we definitively say whether an object in S3 is accessible to the public internet or not? To be honest AWS accounts are a complete mess and the AWS dashboard does not gracefully handle reduced permissions so this is not an inspiring start. The policy framework is everything that explains why formal methods has gotten very little traction in day-to-day software engineering, it is extremely difficult to parse (maybe this is a Z3 problem)
wek
Thank you for this. This seems like a promising approach to agent permissioning. What are the performance implications?