Axiom: A native Calculus of Inductive Constructions kernel in pure Swift

Hi everyone, I wanted to share a project I’ve been working on. While Swift isn't traditionally used for proof assistants, the goal here isn't to replace Lean or Coq. The mission is bringing in-process formal verification to Apple Silicon. Axiom acts as a deterministic gatekeeper for on-device LLMs. Currently, local AI models hallucinate math. The architecture I'm building with Axiom flips this into a tight "model proposes, kernel verifies" loop: the AI generates candidate proof steps (ASTs) a...