Axiom: High-Performance Formal Verification Kernel & SMT Solver

Axiom is an industrial-grade formal verification kernel, SMT (Satisfiability Modulo Theories) decision engine, and program verifier written in Swift. It combines modern DPLL(T)/CDCL(T) lazy constraint solving, Nelson-Oppen multi-theory equality sharing, and Dijkstra weakest precondition semantics with C SIMD acceleration, Python differential testing against Z3, and an interactive HTML5/Canvas proof DAG visualizer.

      ___      _  _ _     ___  ___  __  __
     / _ \    \ \/ (_)___| _ \/ _ \|  \/  |
    / /_\ \    >  <| / _ \   / (_) | |\/| |
   /_/   \_\  /_/\_\_\___/_|_\\___/|_|  |_|
   Formal Verification Kernel & SMT Solver

---

Key Capabilities

• CDCL Propositional Core (AxiomSAT): Two-Watched-Literal (2WL) unit propagation, 1-UIP conflict analysis with asserting clauses, recursive clause minimization, VSIDS exponential decay activity heuristics, and Luby restart schedules.
• First-Order Theory Solvers (AxiomTheories):
  • EUF: Dynamic congruence closure over E-graphs with proof forests.
  • QF_LRA: Dual Simplex over exact arbitrary-precision Rational numbers with Bland's cycling prevention and Farkas certificate generation.
  • QF_LIA: Branch-and-bound integer relaxation, Gomory cuts, and Bezout Diophantine GCD infeasibility refutation.
  • QF_BV: Word-level simplification, bit-blasting, and AIG logic circuit synthesis.
  • QF_AX: McCarthy arrays enforcing ROW1, ROW2, and extensionality axioms via reduction to EUF.
• Cooperating SMT Engine (AxiomSMT): Nelson-Oppen equality sharing fixed-point loop, Delayed Theory Combination (DTC), Unsat Core extraction via assumption tracking, and Craig Interpolation.
• Program Verification Engine (AxiomVerify):
  • Dijkstra Weakest Precondition (WP) predicate transformer calculus.
  • Bounded Model Checking (BMC) with loop unwinding and SSA path compilation.
  • Houdini inductive loop invariant synthesis.
  • Owicki-Gries concurrent thread safety and mutual exclusion verification.
• SIMD Hardware Acceleration (CAxiomKernel):
  • AVX2 (256-bit) and ARM NEON (128-bit) vectorized popcount reductions.
  • Vectorized bitset AND/OR operations and dot-product acceleration.
• Z3 Differential Testing (python/):
  • Randomized SMT-LIB 2.6 grammar fuzzer (smtlib_generator.py).
  • Cross-validation harness comparing Axiom against Z3 (differential_tester.py).
• Interactive Proof DAG Visualizer (web/):
  • Canvas-rendered proof resolution trees, 1-UIP conflict cuts, and live SMT-LIB editor.

---

以上为 README 的开头部分。其余内容请阅读原文。 查看完整 README ↗