Axeyum

Axeyum is a research implementation for answering supported questions about logic, mathematics, and programs with replayable evidence. Its central design separates fast, untrusted search from smaller checkers that validate a result. Unsupported, incomplete, or resource-bounded routes return an explicit unknown.

What is implemented

• A pure-Rust solver and proof stack spanning selected bit-vector, arithmetic, array, datatype, floating-point, string, and quantified fragments
• Bounded program and smart-contract verification with replayed counterexamples
• Certificate-bearing computer algebra and selected proof reconstruction routes
• A fact ledger that records assumptions, artifacts, and validation status
• Browser-native scalar QF_BV queries through WebAssembly

Axeyum is broad but intentionally uneven. It is not presented as a drop-in replacement for Z3, cvc5, Lean, angr, or Unicorn; the repository publishes its current support and trust boundaries alongside the code.