I am currently leading a small team of applied scientists to deliver an innovative new AWS security product powered by GenAI. In this new role, I'm working to establish product direction, define quality metrics that enable rapid iteration, and strengthen the team through hiring and development.Previously:I joined a business-critical tiger team to verify a key block of an upcoming AWS Trainium chip after the departure of a key designer had left an understanding gap. Over four months, I spearheaded documenting the unit's behavior, developed a formal verification environment in Jasper, wrote comprehensive properties, and achieved over 70% full proofs using proof structuring. I found dozens of confirmed bugs and implemented RTL fixes.I led the development of an internal service that helps engineers identify and minimize access to Amazon's most sensitive customer data. Using automated reasoning, this service analyzes policies and network access to uncover possible data flows that an adversary might exploit. My role spanned concept development, team management, product strategy, roadmap planning, and building partnerships with other research and security teams across Amazon.

I can't discuss my work at Apple.

Wrote translator for formally modeling Verilog/SystemVerilog which powered all of Centaur's FV effort and many side tools (linter, equivalence checker, refactoring tool, code browser).Formally specified X86 integer, floating-point, and media instructions and created a high-speed testing framework to validate these specs and reuse them for post-silicon verification.Mechanically proved that Centaur's execution units implement these specifications, revealing many bugs; automated and maintained these proofs as the design has evolved.Designed microcode model with a formal connection to the execution units, and a microcode verification framework with effective proof automation.Developed proof engines for AIG/BDD reasoning, interfacing with SAT solvers, the GL symbolic simulation framework, and core ACL2 libraries for bit vectors, data structures, etc.Created a unified documentation system for the entire FV effort.Many other side projects, usually connecting things which should not be connected.

Wrote the “self-verifying” Milawa theorem prover (dissertation project).Created ACL2 libraries for set theory, linear memories, file operations, unicode, etc.Developed and maintained an ACL2 installer for Windows.

Developed new ACL2 libraries for dependency trees, maps, and functional instantiation.Extended many widely used ACL2 libraries and our build system.

Program transformation research using the High Assurance Transformation System (HATS).Formalized the Sandia Secure Processor (an embedded JVM) in ACL2.Led experimental programming languages course for gifted freshmen.

Developed Research Wizard (LAMP web app) which received national recognition by the American Library Association.Assembled, maintained, and supported 125 staff and public computers.Awarded the library's Distinguished Service Award.

Verification of a static class loader for the Sandia Secure Processor (an embedded JVM).