C L A W Q
The Formally Verified AI Assistant
A formally verified personal AI assistant runtime --- Coq-proven core properties extracted to OCaml, with impeccable manners and machine-checked correctness.
69 theorems verified 18 commands 226 tests
Formally Verified
Core properties proven in Coq with 69 theorems across CLI parsing, configuration validation, path safety, audit chain integrity, and rate limiting.
Extracted to OCaml
Direct Coq extraction pipeline to native OCaml code. Build without Coq installed --- extracted artifacts are tracked in git and verified against drift.
Secure Runtime
Landlock OS sandboxing, token-bucket rate limiting, AES-256-GCM encrypted secrets, HMAC audit chains, and risk-classified tool invocations.