NATP

A Rust-Native Automated Theorem Prover for Finite Sequences

use natp::{claim, theorem, Seq};

theorem()
    .forall::<Seq<i32>>()
    .claim(claim!(|xs| reverse(reverse(xs)) == xs))
    .prove()?
    .require_proven()?;

The kernel produces checkable certificates. The bounded backend verifies claims up to a length limit, and the SMT backend checks obligations with Z3.