Kevin Clancy - Software Engineer
I’m a software engineer looking for opportunities in web development, program analysis, IDE development, and compiler development.
I have experience in C++, Java, Typescript, and Python, and for personal projects, I like to use F#, OCaml, and Rust. I believe in using static type checking, writing demanding functions with strong preconditions and postconditions, and using sum datatypes to make illegal states unrepresentable.
Recent Experience
CertiK
At CertiK, I used Python to develop an abstract interpretation tool on top of the Slither static analyzer for Solidity code. This tool performed both points-to and integer range analyses. The former was used as a basis for taint tracking and many other ad-hoc bug detection tools. The latter was used for detecting integer overflows, division by zero, and unsafe casts. According to activity in CertiK’s custom github branch, this tool was used as recently as Summer 2025. After a year at CertiK, I was promoted to Senior Software Engineer. My deep knowledge of abstract interpretation and order theory made me effective in this role.
Amazon
At Amazon, I developed a CDK project (i.e. infrastructure deployment definition) for an internal web application for tracking releases of Amazon brand devices such as Kindles. I also performed a migration of the device database from an older Amazon-internal database system to DynamoDB. Additionally, I performed maintenance on the business logic that decides when to show Amazon Prime advertisements to customers. After a year at Amazon, I was recruited by CertiK.
Personal Projects
I’m almost always working on programming projects to improve my software engineering abilities. These rarely ever get finished. Here are a few example projects, chosen mainly for recency.
Web Development
Brokenjaw.net message board (github)
Skills: React, Rust, Typescript, HTML, CSS, Loco, SQLite, Docker, Github Actions, AWS, S3, Terraform, Claude Code
I recently created an online message board for discussing jaw fractures, called BrokenJaw.net. This site uses the Rust-based backend framework Loco and the SQLite database system. Its frontend is written in Typescript and uses the React framework. I studied HTML, CSS, and React while developing this site, though the AI-generated frontend code doesn’t keep a clean separation of logical HTML layout and visual CSS styling, opting instead for inline styling. It uses Github Actions to build, test, and deploy docker containers to an AWS EC2 instance each time code is pushed to its github repo.
This website, while currently functional, is a work in progress. I plan to continue refining it over the coming months.
This is the first project that I’ve created using AI-assisted programming tools. In fact, much of the code was written using Claude Code. On one hand, Claude Code has an almost super-human ability to account for complex software contexts while synthesizing new code. It’s also fairly good at getting details correct and writing readable, robust code. Claude Code is a powerful tool that I will continue to use for personal projects in the future.
Languages and Compilers
Game Kitchen - Lua IDE and Type Checker (bitbucket)
Skills: C#, F#, Lua, C++, Type Systems, IDE Development
Types are the most powerful tool I know of for making software more maintainable. When attending the University of Iowa, I read the book Types and Programming Languages by Benjamin Pierce. I applied the knowledge I gained about type systems by designing and implementing an optional type system for Lua. I also created a Lua debugger and an IDE called Game Kitchen, targeted at the Lua game programming framework Love2D. Game Kitchen was written in F#, C#, C++, and Lua.
This is an extremely old project. But I’ve included it because it’s one of the more ambitious projects I’ve worked on, and my software engineering sensibilities haven’t changed much since then. I still believe that functional programming and design-by-contract are important techniques that lead to readable, maintainable software.
The following video is a bit tedious. I don’t recommend watching the whole thing, but you can watch a random point in the video for a couple of minutes to see Game Kitchen in action.
Compilers and VMs
Compiler Design: Virtual Machines by Reinhard Wilhelm and Helmut Seidl (github)
Skills: Rust, Virtual Machines, Garbage Collection
Having already implemented the virtual machine for a C-like language described in Chapter 2, I implemented the Maurer Machine virtual machine for an OCaml-like language described in Chapter 3.
- Higher-order functions
- Curried Application
- Closures
- Mutually recursive functions
- Tuples
- Tail call elimination
I went beyond the material described in the book, adding the following features:
- Mutable reference cells
- Algebraic datatypes, pattern matching, and match expressions with ‘when’ clauses
- A two-space copying garbage collector
Pliron Contributions github
In 2026, I started contributing to a multi-level compilation framework called Pliron. It can best be thought of as a MLIR clone written in Rust. Multi-level compilation provides common infrastructure for pass management, rewriting, and verification across multiple IR lowering phases with different levels of abstraction. This project was conceived and implemented primarily by vaivaswatha; it’s been extremely helpful to learn from someone with far more Rust and compilers expertise than I have.
So far, I have contributed the following to pliron:
Miscellaneous Projects
Schema Types - NoSQL Database Schema Language (github)
Skills: F#, Type Systems, Database Schemas, MUMPS
Before working at Amazon, I worked at a company called Epic Systems, which develops health record software for hospitals. Epic’s software is based on the MUMPS database system. Unlike SQL, MUMPS provides no formal language for specifying database schemas. Therefore, at Epic, schemas are either conveyed informally in a company manual or internal wiki, or they are never defined. A formal schema language allows us to automatically generate validation routines, and it prevents common errors such as coherence errors where a single value may be interpreted in multiple ways.
Schema Types is an experimental schema system for MUMPS, using type syntax to define the structure of MUMPS databases. It expresses the logical layer of the database using a language similar to the calculus of constructions. It expresses the physical layer using something akin to a standard type system, but which references the logical layer using indexed types. I used F# to create a prototype type-checker and test generation tool.