Engineering & research profile

Varun Pant

Amazon Web Services (AWS) · 2026

Varun Pant builds AI products at Amazon Web Services, with a focus on neurosymbolic AI. He explores how formal verification can make generated software easier to trust by checking implementations against explicit specifications.

His approach assigns humans responsibility for the specification while machines help produce code and proofs. He uses Lean to explain the distinction between tactics that construct proofs and the small kernel that checks them, connecting that distinction to practical verification of systems code.

1 conference talk

AI Engineer World's Fair 202610:06

Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS

Varun Pant presents formal verification as a way to check AI-generated code against explicit specifications. He argues that humans should validate specifications while machines produce implementations and proofs. He explains Lean’s tactics and trusted kernel, describes zlib and Cedar examples, and outlines approaches for verifying Rust and other languages.

Varun Pant

References

ai.engineer/talks/lRa9sPaMyy4-your-code-has-bugs-lean4-has-proofs ↗