• Cornell University
  • Computer and Information Science
  • mail [at] jpramos [dot] me


I’m a Junior at Cornell University working towards degrees in Computer Science & Philosophy. I started doing Computer Science research under Dr. Adrian Sampson in the Calyx project. We studied optimizations and extensions towards a compiler infrastructure to simplify encoding of high-level program semantics to lower-level synthesizable hardware designs.

My main research interests involve developing practical tools for software verification using both formal & lightweight methods.

Current Research

Since the summer of 2022, I’ve been working under CMU’s REUSE program with Dr. Jonathan Aldrich. We’ve been working on a Gradual Verifier which serves to bridge the gap between static and dynamic verification, by allowing incremental verification of a program.

My work under the Gradual Verification framework involves optimizing and verifying the soundness of the first ever gradual verification tool – Gradual C0 – and bringing gradual verification to the domain of blockchain programming languages.

Idea of a Certain Cat 2004 -Tokuhiro Kawai (川井徳寛)