Security
Formally verified.
Not just claimed.
Most security claims are tested. InferNode's are proven. Three independent formal verification tools confirm that namespace isolation holds across every possible sequence of operations — billions of states, zero violations.
The Architecture
If you didn't grant it,
it doesn't exist.
Each agent runs inside its own namespace — a view of the world built entirely from resources you explicitly hand to it. Your credentials, SSH keys, email, and private files are not hidden from the agent. They are simply absent. There is nothing to find.
This is not a sandbox bolted onto a conventional OS. It is the original Plan 9 design, refined and formally proven correct. The isolation boundary is structural — enforced at the kernel level, not by policy or by hope.
A prompt injection attack that tries to read your SSH keys gets the same response as asking for a file on the moon. The path does not exist.
The Proof
Three tools. Zero violations.
Formal verification means checking every possible state, not just the ones you think to test. InferNode uses three complementary tools, each catching a different class of flaw.
Abstract specification
TLA+ models the namespace at the highest level of abstraction and proves that isolation holds across every reachable state — exhaustively. The core theorem: a resource mounted after a namespace copy cannot appear in the child unless the child explicitly mounts it. Eleven invariants. Zero violations.
Concurrent protocol
SPIN verifies the namespace under concurrent access — multiple threads running simultaneously in every possible interleaving. It checks for deadlocks, race conditions, and whether an agent can ever escape its container through filesystem traversal. None of these happen.
Real kernel code
CBMC verifies properties directly on the actual C source — not a model of it. Array bounds, integer arithmetic, and isolation guarantees are checked in the real kernel implementation. 113 assertions, zero failures. Runs automatically on every commit.
Cryptography
Built for the post-quantum era.
Quantum-Safe Cryptography
experimentalInferNode ships preliminary implementations of the NIST-standardised post-quantum algorithms — ML-KEM for key exchange and ML-DSA for digital signatures — the algorithms the industry is migrating to now. Both are lattice-based, resistant to quantum attack, and run natively on the same lightweight OS that protects your agents.
This work is not yet recommended for production, but cryptographic agility is a first-class design goal. When classical public-key cryptography is broken, InferNode will already have a path forward.
Want the full technical detail?
All specifications, models, harnesses, and CI scripts are open source. The complete methodology — every tool, every configuration, every result — is documented in the repository.