CryptoPatrick
Figure standing on a frozen landscape looking toward distant mountains and sky

November 10, 2026

Seamless Global Nature

Hi, I’m Patrick. I study mathematics at Chalmers and the University of Gothenburg, and I write about logic, automated reasoning, formal verification and Rust. My current project is Foras, an automated theorem prover written in Rust, and RailCheck, a verification case study for railway interlocking systems.

Research holds longer pieces with interactive figures. Labs are working projects you can try or read about. Agents are my small code projects, one per crate family. The Blog is everything else, newest first.

Research

  1. Proving other people's robots. Five public Robocode robots, written without verification in mind, meet a runtime monitor and Verus. Every one breaks a safety property, and enforcing safety helps some robots and hurts others.

Blog

2025

  1. Agentic Micro Economy Random thoughts on technology and economy.
  2. The Time Lock A group of scientists fight to save their work from an invading force.

2024

  1. Squarings Modulo N per Second A look at roughly estimating the number of squarings mod n that a consumer computer can perform per second.