Eric McCarthy

Eric McCarthy
Contact
e-mail: mccarthy@K.E, where K=kestrel and E=edu
address: see Contact page

Bio

My driving interests are in applying formal methods to AI safety, and applying AI to accelerate formal methods.

I believe we must verify the software stacks used by AI models as soon as possible, to prevent theft and misuse as well as to prevent model self-exfiltration. To do that, we need to accelerate formal methods with AI agent help.

On the former I work on language security for ACL2, on formalization of programming language syntax, semantics, analysis, and transformation, such as formal derivations of C code, and formal verification of zero-knowledge circuits such as R1CS and AIR.

On the latter I have been improving an MCP server for ACL2, and I worked on a government-funded project where we trained an early transformer model to give advice to ACL2 users on how to fix failed proofs.

Since different formal methods have different capabilities, I believe for critical projects it is important to apply a variety of methods to achieve higher assurance. My main theorem prover is ACL2, and I hope to work on connecting other provers to ACL2.

I am currently working on a government-funded project where we are synthesizing network filters to protect devices that have unpatched vulnerabilities. I am also working on a government-funded project where we are formalizing the Remora → MLIR compiler.

My past work, inside and outside Kestrel, includes:

  • Development of the Syntheto formal language and safe communication between its IDE and an ACL2 server, on the DARPA MIDAS project.

  • Formalization of parts of Aleo.

  • Formalization of parts of Zcash that are also used by Tezos.

  • Formalization of parts of the Yul intermediate language for Ethereum.

  • The ACL2 Ethereum project.

  • The DerivationMiner project, where I developed (in Python) the “big code” pipeline we used to process and run machine learning on a corpus of 23 TB. I saved Java bytecode and artifacts to a Titan graph database, and ran NMF for dimension reduction. I also developed our code similarity search tool. I would like to apply these “big code” tools to corpora of smart contract code. I also learned how to use the ACL2 theorem prover and did some formal verification as part of this project.

  • The VIBRANCE project, where we automatically hardened Java bytecode against attacks from tainted inputs.

  • With Decidable Software, developed a tool using Software Refinery to automate a large source code port from a proprietary PL/I-like language to standard COBOL for a French customer. Recruited two additional full-time developers for this project.

  • Architect and lead developer for tools used in reinspection service, written in Python and Java. (Reasoning, post-Y2K era)

  • Implemented a distributed processing system for large analysis jobs. (Reasoning, Y2K era)

  • UX/UI design and implementation for Y2K analysts. (Reasoning, Y2K era)

  • Extended Intervista UI toolkit and Dialect grammar compiler to handle Japanese text. (Reasoning, Software Refinery era)

  • Software Refinery core developer for 15 years, bringing into production the Refine IDE, Dialect grammar compiler, Intervista UI toolkit, REFINE/Ada, REFINE/C, REFINE/COBOL, and REFINE/FORTRAN static analysis products. Programming in Lisp and Refine.

I received a degree in Mathematical Sciences from Stanford University in 1984.