Build Axeyum and check a result

Build from source

The default build uses Rust and has no C or C++ dependency.

$ git clone https://github.com/mjbommar/axeyum.git
$ cd axeyum
$ cargo run -p axeyum-solver --features full --example first_smtlib_query

Solve an SMT-LIB query

Save this query as factor.smt2. It asks for two 8-bit values whose product is hexadecimal 2b.

(set-logic QF_BV)
(declare-const x (_ BitVec 8))
(declare-const y (_ BitVec 8))
(assert (= (bvmul x y) #x2b))
(assert (bvugt x #x01))
(assert (bvugt y #x01))
(check-sat)
(get-model)

$ cargo run -q -p axeyum-bench --bin axeyum -- factor.smt2
sat
(
  (define-fun x () (_ BitVec 8) #b11111001)
  (define-fun y () (_ BitVec 8) #b01000011)
)

Inspect the replayed model

The result is sat. The model assigns 249 to x and 67 to y. Their product is 16,683, which equals 43 modulo 256. Axeyum evaluates the model against the original assertions before reporting it.

Source: factor.smt2 recorded model replay @ a103b3db3, 2026-09-03.

Validate the fact ledger

The validator reads every fact file. It checks the schema, evidence rules, proof route, and status. It exits with a nonzero status when a check fails.

$ python3 scripts/validate-facts.py

Use the status page for the recorded totals and proof-route counts.

Run the repository checks

The aggregate checks require different host tools. Confirm the available toolchain before comparing results.

$ just check
$ ./scripts/check.sh
$ cargo test -p axeyum-solver --features full --test corpus_regression
$ cargo test --workspace --lib