01
Boolean satisfiability
Axeyum SAT Solver
A native CDCL solver with AIG and CNF lowering and certificate support.
- CDCL search and learned clauses
- AIG construction and simplification
- CNF lowering
Components
Five systems implemented by Axeyum
Axeyum implements its own SAT solver, SMT solver, computer algebra system, proof kernel, and formal library. The established systems named on these pages are reference points for function and measurement; they are not runtime components.
02
Satisfiability modulo theories
Axeyum SMT Solver
A typed SMT implementation with rewriting, theory solving, bit-blasting, models, and certificates.
- Typed terms and SMT-LIB parsing
- Query planning and rewriting
- Bit-vector, floating-point, string, and arithmetic routes
03
Computer algebra
Axeyum CAS
A proof-carrying computer algebra system for exact symbolic operations.
- Exact polynomial and rational-function operations
- Differentiation and certified integration
- Exact algebraic real witnesses
04
Proof checking
Axeyum Kernel
An independent Rust checker for a selected Lean-core term language.
- Dependent terms and universe levels
- WHNF and definitional equality
- Inductive types and recursors
05
Formal mathematics
Axeyum Library
A dependency-aware library of checked facts with explicit evidence and assumptions.
- Typed fact records and semantic validation
- Direct dependency and dependent edges
- Proof-route and evidence metadata
Components and crates
A component is a public system boundary. A crate is a Rust implementation boundary. The SMT Solver therefore has one public page even though parsing, typed terms, rewriting, bit-vectors, floating point, strings, and search are implemented in separate crates.
Results remain separate from component descriptions. Open a component to find its crates, current limit, comparison report, and related problem studies.