Resume
Alan Wisper, Rust & formal verification engineer
My experience as a Rust software engineer who works on formal methods, language runtimes and backend: what I focus on, what I've done in open source, where I've worked and what I work with. Company names are left out of this public version; I'll share them on request.
Sacramento, CA · Authorized to work in the U.S. without sponsorship
Focus
Formal verification engineer, for software
Lean 4, HOL4, Kani, and the code they check.
Software engineer focused on formal verification, language runtimes, backend and developer tools. Works on formal methods with Lean 4, HOL4 and Kani and contributes to these systems, including the CakeML verified compiler and the Poly/ML garbage collector. Before that, at a U.S. startup, built Node.js API compatibility, web standards and database access for guest languages in a polyglot runtime on Rust and GraalVM. Led infrastructure teams and used to taking code from spec to release.
Open source
Work in open source
A verified compiler, a runtime, a Postgres extension, a library with proofs.
CakeML
Made the stack of compiled programs non-executable on Linux and fixed four bugs in its Pancake language. All five pull requests merged.
Poly/ML
Diagnosed and fixed a garbage-collector heap-sizing bug that crashed parallel HOL4 builds with “Run out of store”: 2 failed builds in 60 before the fix, 0 in 180 after. Merged by the author of Poly/ML.
ParadeDB
Fixed index builds, inserts and search that broke on infinite dates, and wrong rows or overflows at the edges of the bigint range, both with tests. The date fix shipped in release 0.26.1.
lethewis
Key-handling library with safety properties proved in the Kani model checker.
Experience
Where I've worked
Language runtimes, backend, infrastructure.
Software Engineer (Contract)
The startup builds a polyglot runtime (Rust/GraalVM core) that runs JavaScript/TypeScript, Kotlin, Java and Python as a drop-in alternative to Node.js and JVM build tooling.
- Built the runtime's MySQL and PostgreSQL connectivity layer (JDBC, HikariCP pooling) with full GraalVM Native Image support; added 1,136 tests across 116 files.
- Built a Node.js conformance harness from the official Node.js test suite and raised measured conformance from 25% to 72% across core runtime modules.
- Implemented Node.js core modules (net, http/https/tls, dgram, dns, fs, streams, crypto, child_process) and the WHATWG Fetch, Streams and URL standards.
- Implemented and debugged native functionality in the Rust runtime core under GraalVM Native Image constraints.
- Fixed the broken release pipeline, added npm and APT publishing, and resolved cross-platform packaging issues including Linux glibc compatibility.
- Reviewed 30+ pull requests on core infrastructure, including a GraalVM upgrade and packaged installers; ran a codebase quality audit and drove the resulting issues.
Software Engineer
- Designed and built a full ERP system from scratch (C#, PostgreSQL) covering inventory, supply chain, sales, accounting and manufacturing.
- Built a data pipeline that consolidates supplier e-commerce data into a normalized PostgreSQL schema for analytics and BI.
- Led the e-commerce migration from Shopify to PrestaShop, including the full catalog transfer and API integrations.
- Built automated reporting dashboards that replaced manual reporting across departments.
Lead Systems Engineer
- Led a team of 19 engineers; modernized 28 physical and 477 virtual servers (KVM/QEMU, Docker Swarm, Zabbix).
- Migrated 60% of the infrastructure to Linux, cutting license and hardware costs by $63K a year.
- Led development of a microservice-based internal asset-management platform (C#/.NET Core, Docker Compose).
- Automated workstation provisioning and patching with Ansible.
IT Architect & Infrastructure Consultant (Freelance)
- Built internal dashboards and frontends with Vue.js, TypeScript and Go (Gin) for real-time infrastructure monitoring.
- Developed tools and microservices in C# (.NET Core), JavaScript, Python, Go and PowerShell, integrated with CI/CD and infrastructure APIs, cutting manual admin work by over 60%.
- Designed hybrid cloud and on-prem infrastructure (50–1,000+ users) for healthcare, fintech and logistics clients, cutting cloud costs by up to 79%.
- Implemented CI/CD pipelines (Ansible, GitLab CI/CD) that cut deployment time by 40%.
Earlier experience
Systems Architect and Systems Administrator roles: multi-site network and directory infrastructure, hardened mail infrastructure, and internal tools in Python and C#/.NET.
Skills
Technical skills
A Rust engineer, with TypeScript, Go and Python close at hand.
- Formal verification
- Kani, HOL4, Lean 4
- Languages
- Rust, TypeScript/JavaScript (Node.js), Go, Python, C#, Java, Kotlin, C++, Standard ML, SQL
- Runtimes & systems
- GraalVM Native Image, Node.js internals, WHATWG web standards, garbage collection
- Backend & data
- PostgreSQL, MySQL, SQLite, JDBC/HikariCP, REST, WebSockets, event-driven architecture, JWT/RBAC
- Frontend
- Vue.js, React, Astro, HTMX
- Infrastructure
- Docker, GitHub Actions, Ansible, AWS, Cloudflare Workers
- Security
- TLS, IAM/MFA, WireGuard/IPsec, HIPAA-compliant systems, hardening
Education
Two master's degrees
Computer systems and systems engineering.
Master's, Computer Systems Analysis
Master's, Systems Engineering
Hiring a Rust & formal verification engineer?
The PDF is the same resume, for your files. Or write to me: I reply within a day.