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.
380 theorem/lemma statements 43 commands 3293 tests
Formally Verified
The Coq corpus now tracks 380 theorem/lemma statements, including 380 in completed verification areas and 0 more under active development.
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.
Precision Timepiece