Hi HN. I built IC-AGI because every AI agent framework I looked at gives the agent full authority once it gets an API key. That's fine for demos but scary for anything touching production data or infrastructure.
IC-AGI splits authority using K-of-N threshold approval (Shamir Secret Sharing). No single node, human or AI, can unilaterally execute a critical action. Capability tokens have TTL, scope, and consumable budgets, so an agent can only do what it was explicitly authorized to do, for a limited time, within a spending cap.
The part I'm most interested in feedback on: I formally verified 14 safety properties using TLA+ model checking (~50K states, ~250K property checks) plus 8 algebraic proofs for the Shamir implementation. Zero violations. If you work with TLA+ or formal methods, I'd love to hear if my specs are sound or if I'm missing edge cases.
Stack: Python, Shamir SSS over GF(p), HMAC-SHA256, FastAPI control plane, K8s manifests for distributed workers. 273 tests including adversarial attacks (replay, MITM, oracle extraction, code injection). Apache 2.0.
saezbaldo•1h ago
IC-AGI splits authority using K-of-N threshold approval (Shamir Secret Sharing). No single node, human or AI, can unilaterally execute a critical action. Capability tokens have TTL, scope, and consumable budgets, so an agent can only do what it was explicitly authorized to do, for a limited time, within a spending cap.
The part I'm most interested in feedback on: I formally verified 14 safety properties using TLA+ model checking (~50K states, ~250K property checks) plus 8 algebraic proofs for the Shamir implementation. Zero violations. If you work with TLA+ or formal methods, I'd love to hear if my specs are sound or if I'm missing edge cases.
Stack: Python, Shamir SSS over GF(p), HMAC-SHA256, FastAPI control plane, K8s manifests for distributed workers. 273 tests including adversarial attacks (replay, MITM, oracle extraction, code injection). Apache 2.0.
Longer writeup with the threat model: https://dev.to/saezbaldo/every-ai-agent-framework-trusts-the...
Happy to answer questions about the architecture or the formal verification approach.