Formal verification for AI is fascinating, but the real challenge is runtime verification of AI agents.

Example: AI browser agents can be exploited via prompt injection (even Google's new "User Alignment Critic" only catches 90% of attacks).

For password management, we solved this with zero-knowledge architecture - the AI navigates websites but never sees credentials. Credentials stay in local Keychain, AI just clicks buttons.

Formal verification would be amazing for proving these isolation guarantees. Has anyone worked on verifying AI agent sandboxes?