tpt-formal-lab

Proof-native, verification-first building blocks for safety-critical Rust.

---

tpt-formal-lab is a workspace of five focused crates for developers building systems where floating-point errors, non-determinism, or logical flaws are unacceptable — flight control, financial engines, cryptographic protocols, and formally verified compilers.

Crates

Crate	Description	crates.io
tpt-exact-math	Arbitrary-precision rational numbers and interval arithmetic
tpt-proof-ast	Strongly-typed proof-native AST — invalid states are compile errors
out-verify-macros	Procedural macros for #[requires], #[ensures], #[invariant]
tpt-deterministic-sim	Bitwise-deterministic simulation engine
out-smt-bridge	Ergonomic Rust → SMT-LIB2 bridge for Z3, CVC5, etc.
tpt-redundancy	N-modular redundancy and voting for fault-tolerant systems
tpt-verified-ode	Rigorously verified ODE integration via interval arithmetic
tpt-trace-macros	#[traces("REQ-…")] macro linking code to requirements
tpt-verified-algorithms	Verified sorting and searching with debug-mode contract checks
tpt-det-proptest	Deterministic property-based testing with bisection shrinking

---

Quick look

Exact arithmetic — no rounding ever

use tpt_exact_math::Rational;

// 0.1 + 0.2 is exactly 3/10 — not 0.30000000000000004
let a = Rational::from_frac(1, 10);
let b = Rational::from_frac(2, 10);
assert_eq!(a + b, Rational::from_frac(3, 10));

Type-safe AST — invalid trees don't compile

use tpt_proof_ast::{AstBuilder, Formula, Term};

let b = AstBuilder::new();
let x = b.var_term("x");
let stmt = b.forall("x", b.gt(x, b.int_term(0)));
// You cannot accidentally use a Term where a Formula is expected.

Formal contracts — zero runtime cost in release

use out_verify_macros::{requires, ensures};

#[requires(x > 0)]
#[ensures(result > 0)]
fn double(x: i32) -> i32 { x * 2 }

Bitwise-deterministic simulation

use tpt_deterministic_sim::{DeterministicSim, FixedPoint};

type Fp = FixedPoint<1_000_000>;
let mut sim = DeterministicSim::<Fp>::new();
// Identical on x86, ARM, RISC-V — guaranteed.

SMT solver interface — pure Rust, no C

use out_smt_bridge::{SmtSolver, Sort, Expr};

let mut solver = SmtSolver::new();
solver.declare_const("x", Sort::Int);
solver.assert(Expr::gt(Expr::var("x", Sort::Int), Expr::int(0)));
println!("{}", solver.emit_check()); // pipe to z3 -in

Verified voting — tolerate faulty channels

use tpt_redundancy::Replicated;

let channels = Replicated::new([10u32, 10u32, 12u32]);
assert_eq!(channels.majority_vote().value(), Some(&10u32));

Verified ODE integration — enclosures, not floats

use tpt_exact_math::Rational;
use tpt_verified_ode::OdeSolver;

let mut solver = OdeSolver::new(|_t, y| y.clone(), Rational::from(0), Rational::from(1));
let (lo, hi) = solver.step(&Rational::from_frac(1, 4)); // contains e^0.25
assert!(lo <= hi);

Requirement tracing — link code to specs

use tpt_trace_macros::traces;

#[traces("REQ-BRAKE-001")]
pub fn braking_distance(speed: f64) -> f64 { 0.5 * speed * speed }

Verified algorithms — checked postconditions

use tpt_verified_algorithms::verified_sort;

let mut data = [3, 1, 2];
verified_sort(&mut data);
assert_eq!(data, [1, 2, 3]);

Deterministic property testing — reproducible by seed

use tpt_det_proptest::{check, IntRange, Seed};

let r = check(100, Seed(1), IntRange::<i32>::new(0, 100), |x| *x < 100);
assert!(r.is_ok());

---

Getting started

Add the crates you need to your Cargo.toml:

[dependencies]
tpt-exact-math      = "0.1"
tpt-proof-ast       = "0.1"
out-verify-macros   = "0.1"
tpt-deterministic-sim = "0.1"
out-smt-bridge      = "0.1"
tpt-redundancy      = "0.1"
tpt-verified-ode    = "0.1"
tpt-trace-macros    = "0.1"
tpt-verified-algorithms = "0.1"
tpt-det-proptest    = "0.1"

MSRV

Rust 1.75 or later.

License

Licensed under either of MIT or Apache-2.0 at your option.