Skip to content

§ Capabilities

Verification & correctness

Establishing that software does what it claims — by proof where the domain allows it, and by disciplined measurement everywhere else.

  • Kani (bounded model checking)
  • Verus (linear ghost types)
  • Miri (undefined-behaviour detection)
  • Property and invariant design
  • Reference-equivalence testing
  • Deterministic PRNG design
  • Playwright end-to-end testing
  • Jest / Vitest
  • Mechanical quality gates