Harmonic Engineer Showcases Aristotle Formal Verification Wins

At the University of Glasgow, Satnam Singh of Harmonic demonstrated his AI-based Aristotle verification system proving the correctness of Ibex RISC-V core MUL operations and the memory safety of OpenTitan's root-of-trust C code.

2026-10-30 ~ 2026-10-31 · 3 related posts

• Harmonic Engineer Satnam Singh to Give Glasgow Talk on Why Formal Verification Is On Fire — satnam6502 · 2026-10-30
• Aristotle system machine-checks Ibex RISC-V core MUL operation formally — satnam6502 · 2026-10-31
• AI formal verification: Aristotle proves memory safety of OpenTitan root-of-trust C code — satnam6502 · 2026-10-31