I've refreshed my project ideas for incoming CST Part II and MPhil students who are starting in October 2026 (term's starting soon!). As ever, these aren't an exhaustive list but a good starting point for things we might work on together. See also Srinivasan Keshav's own list for even more.
The open projects fall into two rough batches: applying compsci to solve difficult environmental problems, and more conventional systems / programming languages work on verification, effects or unikernels. Almost everything on the list is pitched at an MPhil-level project, but it's fairly easy to pitch it up and down to a Part II/III depending on your enthusiasm.
You have a much better chance of getting my attention if you show evidence of thinking and researching the idea a bit before getting in touch. I unfortunately receive dozens and dozens of LLM-generated CVs a week these days and easily miss generic messages.
1 Tough planetary computing projects
I want to point to three of the Tessera ideas in particular, because it's a great time to be working in this field. The last year has seen a huge surge of interest in geospatial foundation models.
"Generative detection of ghost roads" introduces a problem that seems easy: surely we should easily be able to spot all roads from space? A great many roads simply aren't mapped, especially in the tropics, and road building almost always precedes forest loss events. The 2024 study that established this took some 7,000 hours of volunteer effort to hand-map the tropical Asia-Pacific, and found between three and six times more roads than the global datasets knew about.
Where this project comes in is that per-pixel and patch classifiers are throwing away the most obvious thing we know about roads, which is that roads connect to other roads. This structural prior means we can experiment with some fun machine learning approaches to bolt topology-preserving losses onto a segmentation head, so the output is a network. We could also try the RoadTracer technique, and have an agent walk outwards from known seeds, deciding at each step whether the road continues. Or we could treat crowd-sourced data like OpenStreetMap as a partial graph and train a model to propose missing edges, sampling repeatedly to get a distribution over where unmapped roads might be.
"Generating potential natural vegetation maps" asks what the land surface of the world would look like today if humans hadn't existed. Global species extinction metrics like LIFE (paper) need baselines like this to determine the impact of human actions. And more locally, we could also use a 'what-if' machine to figure out the impact of (e.g.) replacing an agricultural field with a forest on the local biome.
This is quite a challenging machine learning problem since we need to find the (current) parts of the planet unaffected by humans, and then learn how climate, terrain and soil relate to what the land surface does when it is left alone, and then apply generative techniques to the now-human regions. It builds directly on our global habitat mapping work. Validation could start with held-out wild regions and comparisons against the existing PNV maps, and we'd have to brainstorm further ideas for a map generated using current climatic conditions...
"Interpretable downscaling of local weather predictions" is a lot of fun if you want to get into matters of both climate and biodiversity! We now know from Pedro Sousa's work that satellite embeddings improve local forecasting significantly, but not why. We need to explore techniques where we can attribute the gained accuracy back to recognisable surface properties in the Tessera embeddings, or turn the problem around and figure out how to ascribe weights to individual station observations. This would be great fun for anyone interested in diving into probabilistic modelling.
"Scanning the literature for species range and habitat maps" is one for LLM and VLM aficionados. We're building an agentic pipeline over the millions of conservation fulltexts in Evidence TAP to recover habitat classes, elevation limits and range polygons for taxa that have never had a Red List assessment. There's a lot of difficult vision work here, since these papers have (sometimes hand-drawn) diagrams where some obscure knowledge about a species was recorded 50 years ago. Quite often, the range maps are georeferenced with respect to some local landmarks. This project suits someone interested in evaluation design and in getting VLMs to behave over long documents.
"Agentic LLMs and local field guides" is for the birders among you! Anyone who's been travelling knows that the local guides have much more information about a given region than a general book. So rather than training massive classifiers, we're working out whether a multimodal model given a regional field guide ('The Birds of Peru') can do VLM search and reason its way to an identification. This long tail (pun intended) of local species is often where biodiversity occurrence sightings are weakest, and so improving performance there will make a big difference to the accuracy of species mapping, and to efforts like a living IUCN Red List.
2 Systems and programming languages
Systems and PL work remains very much of interest, of course; there's plenty to be done! Here are some of the things I've been thinking about recently:
- Compiling Lean specifications into OxCaml enforcement automata (MPhil). Write a cross-layer effect specification once in Lean 4 as a Dijkstra monad, then compile it into proof obligations as well as a runtime automaton in OxCaml, with a proof that the latter represents the former. I did a much cruder version of this twenty years ago with SPL. Suits someone who wants both proofs and executable fast code.
- An io_uring backend for Lean (MPhil). What the heck does a shared memory protocol have to do with a proof assistant, I hear you ask? Lean 4 can emit executables, but they currently do slow blocking IO. I thought it'd be fun to not only specify the submission/completion ring pair in Lean itself, but also to wire it up into the runtime and prove properties about the single-producer/single-consumer invariants. See my post-POSIX talk for some background.
- An antibotty defensive testbed (MPhil). The time-to-exploit a vulnerability is now negative. This project asks whether a mitigation to some cyberattack can be synthesised, verified and deployed faster than an agent can write the exploit in the first place! I was thinking about a small total rule language with safety obligations, and enforced by a MirageOS gateway. Suits someone interested in doing lightweight formal methods and some unikernel plumbing to get some systems experience.
- A hardware description language using OCaml effects (MPhil). HardCaml builds a circuit as a data structure via some fairly demanding module-system work. Could OCaml 5 effect handlers let us instead describe the circuit by evaluating it directly, as Clash does? This suits someone with an interest in language design who wants to get into hardware design.
Most of these have supervisors beyond just me who have expertise deep in the adjacent fields. Several of the projects also sit beside larger programmes in my group such as TESSERA, Enki, OxCaml or Conservation Evidence, where you have loads of other people to talk to.
So get brainstorming, and I'm looking forward to seeing you all at the start of term!
