Software engineer focused on formal verification, security and encryption, as well as runtimes, backend and developer tools. Work on formal methods with Lean 4, HOL4 and Kani and contribute to these systems. My Rust project lethewis uses Kani to prove safety properties of encryption-key storage. 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 projects as part of regular team work.
Looking for backend, systems, runtime, security or formal verification work at a startup.
Remote: Yes
Willing to relocate: Likely yes
Technologies: Rust, Go, TypeScript, Python, C++, Standard ML; Lean 4, HOL4, Kani; GraalVM, Node.js internals; PostgreSQL; Docker, AWS, Cloudflare Workers
Résumé/CV: https://alanwisper.com/resume
GitHub: https://github.com/wisper-dev
X: https://x.com/alawisper
Email: hi.wisper [at] gmail [dot] com
Software engineer focused on formal verification, security and encryption, as well as runtimes, backend and developer tools. Work on formal methods with Lean 4, HOL4 and Kani and contribute to these systems. My Rust project lethewis uses Kani to prove safety properties of encryption-key storage. 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 projects as part of regular team work.
Looking for backend, systems, runtime, security or formal verification work at a startup.