Jared Davis

I’m taking 2026 as a sabbatical to focus on independent research, creative passion projects, and technical exploration.

From 2024-2025, I led a small team of 4-8 applied scientists and security engineers to deliver the AWS Security Agent which launched at re:Invent 2025. As a player-coach, I worked on everything from product direction, project planning, implementation approaches, and evaluation metrics to enable rapid iteration. I also worked to strengthen the team through hiring and development. Earlier in 2024, I joined a business-critical tiger team to verify a key block of AWS Trainium3 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. Prior to that, 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).