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) and the Axiom kernel type-checks them in the same address space, ensuring only mathematically valid steps survive.
Architecture & Memory Model
The key design choice for this use case has been leveraging Swift's arena-backed Term handles (as structs) combined with a TermPool and GlobalTypeCache for hash-consing.
When an LLM searches for a proof tree, it constantly generates overlapping sub-proofs. Because Axiom hash-conses terms, rebuilding a deeply nested application spine that the kernel has seen before turns into an O(1) cache lookup. In my benchmarks on Apple Silicon, evaluating heavily shared spines hits ~15M ops/sec (on repeated shared terms with cache hits, release build) because the validation of repeated structural paths becomes nearly zero-cost.
What the kernel covers today:
- Predicative universe hierarchy (handling Type:Type avoidance)
- Dependent function types (Π-types) and β/δ-reduction
- Inductive definitions with strict positivity and universe policy
- Dependent pattern matching with structural termination
- Unification for metavariable hole resolution
- Sealed declaration boundary and fuel-bounded normalization
On the testing side, I focused on classic edge cases (Girard and Hurkens paradoxes), capture-free substitution via de Bruijn indices, and running differential checks against Lean 4’s kernel on randomized terms.
Current Limitations: To be fully transparent, this is still a minimal fragment.
There is no η-conversion, no let, no Prop, and no parser or tactics yet. Soundness evidence currently relies on rigorous engineering, tests, and Lean differentials (not a formal certificate).
Roadmap: Metal-Accelerated Fuzzy Search
While not implemented yet, the next phase is to move the fuzzy semantic retrieval of proof states to Metal compute kernels. By keeping the fast probabilistic search on the GPU and the deterministic O(1) type-checking on the CPU (with zero-copy overhead via Unified Memory), the goal is to create a massively parallel, self-correcting reasoning engine directly on-device.
I would love to get feedback from the compiler and language enthusiasts here regarding AST memory layout, handling deep recursive normalization without blowing up the stack, and optimizing value-type sharing.
Repository: GitHub - acemoglu/Axiom: Native Swift CIC kernel for embedded proof checking on Apple platforms. · GitHub
Looking forward to your thoughts!