Moving theorem proving upstream into compilers, sandboxes, and the browser seems like the future when we're dealing with increasingly sophisticated AIs. I'm working on similar formal methods but applied to agent sandboxing; do you see Z3 as a better fit than lean? https://github.com/coproduct-opensource/nucleus
I'm building Nucleus for exactly this problem - using information flow control and formal methods, we can prevent confused deputies by proofs instead of heuristics.
Everyone agrees that agent security is an area that needs significant improvement, and quickly. Using methods from information flow control, this is a lightweight demo of how web search can taint a Claude session so it doesn't allow writing after a accessing untrusted data.
This can be configured via profiles to more more or less restrictive.
Treat this as an example for now, more to come in the future.
Thanks! Currently network identity is host-based, but in the middle of introducing SPIFFE based on ZTunnel. Should be done in the next couple of days.
Runtime enforcement means that any side effects are routed through a proxy (nucleus-tool-proxy) that does realtime checks on permissions and gates the behavior.
SPIFFE for MicroVM agents is a compelling idea and I'll update when this is ready.
In this the protagonist discovers he is special, exceptional. He devotes time to thinking and researching career goals and world-changing ideas. Dreaming of reification and being lauded as the (Gauss|Galois|Mozart) of his generation, the present may be bleak, but the future is glorious.
Act II: The Crisis
In this, the protagonist discovers that he is challenged for his position. Others, caught up in the race of life, don't look deeply to see his talent, and communion with the muses is precious only as long as it relates to engineering goals. He is human, suffering financial and relational setbacks, feeling the muses have deserted him and he is fully mortal after all.
Act III: The Resolution
In this, the protagonist discovers he is not alone. Others around him, few to be sure, are equally talented and working to achieve their purpose. Perhaps he's at the 99.9th percentile and realizes there are still 6 million contemporaneous peers. Einstein, Crick, and Jobs all went through this before their breakthroughs. The protagonist finds a passion, gives it his heart and soul, and achieves Movement I of his life story.
Thanks for the excellent suggestions. My local transit agency doesn't have a reputation for complexity, but I'll do some research.
Yes, a startup would certainly offer the complexity I'm after. I'm not pursuing insurmountable complexity in its own right. I feel we should be doing programming at a vastly higher level of abstraction.
Maybe I ought to shift to Haskell development, or spin higher level of abstraction into a venture of its own. Thanks again.