Research
Notes and experiments at the boundary of mathematics, machine learning, and security. Every figure is interactive and every number is computed in your browser.
- 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.
- Who checks the spec? A proof only rules out bugs relative to its spec. Mutation-testing the Verus specs of a robot tank found a robot that never fires and still met its firing spec.
- Fire, but verify. Learning Verus, a verifier for Rust, by proving that a robot tank never fires unsafely. The proof went through. The robot shot itself dead anyway.
- Open Problems and Open Unknowns A certificate criterion for partitioning the unsolved in mathematics, for an age when machines can state conjectures faster than anyone can read them.
- Who checks the Checker? Let's see what happens when an AI requirement quality checker analyzes three requirements sourced from a science fiction story. Will its suggested changes hold up to its own scrutiny?
- Generate, but verify. A language model translates railway safety rules into logic. Two independent theorem provers decide whether it got them right.