Varun Pant

Varun Pant builds AI products focused on neurosymbolic AI, combining language models’ ability to generate software with formal methods for checking precisely stated requirements. His public work at Amazon Web Services connects engineering and product leadership with a practical question: how can developers trust code when agents produce it faster than people can review it?

Defining correctness before proving it

In his 2026 talk on formal verification, he described building AI products and leading teams working on formal verification at AWS. He argued that tests cover selected inputs, model-based judgments remain probabilistic, and human review struggles to match the volume of generated code. Formal verification offers a different kind of assurance: a proof that an implementation satisfies specified properties for every input covered by the formal model and its assumptions.

Pant places human ownership of specifications at the center of this workflow. A developer can write requirements directly in a formal language or let an agent translate natural-language requirements into a formal specification. The developer must then inspect that specification, whether through direct review or checks against representative inputs. A proof cannot rescue a requirement that misstates the intended behavior. Once the specification is validated, machines can produce the implementation and construct its proof. This makes deciding what correctness means an explicit engineering task.

Lean provides a concrete account of how that division works. Definitions and proofs use the same language, while tactics search for ways to establish a theorem and a small trusted kernel checks the resulting proof. Pant compares tactics to chess moves: they explore branches, encounter dead ends, and backtrack. The kernel checks the completed result independently of the search that found it. This separation allows sophisticated proof-generating automation without requiring developers to trust every part of that automation as a proof checker. His list-reversal example makes the guarantee tangible: reversing two concatenated lists produces the reversed second list followed by the reversed first, for every list covered by the theorem.

Verification across existing codebases

• Translating C into Lean: He develops this explanation through examples that involve different relationships between specifications and production code. In the talk’s zlib example, AI translated a C compression library into Lean and generated a proof around a round-trip requirement: decompressing compressed data should recover the original input. The system broke the proof into helper lemmas, proved those smaller goals, and assembled a theorem for the kernel to check. Pant reported roughly 32,000 lines of proof. He presented this as an example of automated proof construction, without claiming authorship of the conversion.
• Modeling authorization policies: Cedar, the authorization policy language, illustrates a strategy that keeps Rust in production. Its formal model is written in Lean, and randomized differential tests check whether the model and Rust implementation produce the same outputs for the same inputs. Pant uses the rule that a satisfied prohibition must override permission to explain why precise semantics matter: an authorization request must be denied whenever an applicable forbid policy is satisfied. Proving properties of the model and testing the implementation’s agreement with it provide distinct forms of assurance; differential testing alone does not prove equivalence for every input.
• Verifying Rust: Pant also explains ways to verify Rust more directly. Verus expresses requirements as preconditions and postconditions alongside code, then uses the Z3 solver to check them statically; verification annotations are erased at runtime. Another approach translates Rust’s intermediate representation into a functional form in Lean, where theorem-proving tools can analyze it. These examples show engineers how verification can fit existing language choices rather than requiring every system to be rewritten in Lean.

Shared tools and maintainable proofs

In 2026, Pant described AWS’s work on Strata, an open-source verification platform under development. Its architecture lets language-specific dialects represent programming constructs and lower them into a shared core written in Lean. Shared representations make analyses and transformations reusable and provide interfaces to reasoning tools. Pant outlined a path to Lean proofs, SMT solvers, and model checkers; the supplied project evidence describes a verification pipeline using symbolic evaluation and SMT solvers. Strata represents collaborative infrastructure work, rather than a project attributed solely to Pant.

His work also addresses the cost of maintaining proofs after they first succeed. Pant shares competition-chair responsibilities with Simon Frieder and Jialin Lu for VeriCodeGen’s 2026 Lean proof-refactoring competition. Its criteria include proof size, elaboration efficiency, and continued compilation across Lean toolchains—practical concerns for keeping verified software usable as its tools change. He also served as an Amazon-affiliated judge at the University of Washington’s 2026 Lean Hackathon. These activities complement his emphasis on making specifications inspectable, proofs independently checkable, and verification practical for working engineers.