# Open MPhil/Part II student projects for 2026-2027
*2026-09-09 — note*
I've refreshed my [project ideas](/ideas) for incoming [CST Part II](https://www.cst.cam.ac.uk/teaching/part-ii) and [MPhil](https://www.cst.cam.ac.uk/teaching/masters) 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](https://svr-sk818-web.cl.cam.ac.uk/keshav/wiki/index.php/Main_Page)'s [own list](https://svr-sk818-web.cl.cam.ac.uk/keshav/teaching/projects.html) for even more.
The open projects fall into two rough batches: applying
compsci to solve difficult [environmental problems](https://anil.recoil.org/projects/plancomp), and more
conventional systems / programming languages work on verification, effects or [unikernels](https://anil.recoil.org/projects/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.
## Tough planetary computing projects
I want to point to three of the [Tessera](https://anil.recoil.org/projects/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](https://anil.recoil.org/notes/geotessera-a-year-on) in geospatial foundation models.
["Generative detection of ghost roads"](https://anil.recoil.org/ideas/tessera-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](https://doi.org/10.1038/s41586-024-07303-5) 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](https://arxiv.org/abs/1802.03680) 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"](https://anil.recoil.org/ideas/tessera-pnv) asks what the land
surface of the world would look like today if humans hadn't existed.
Global species extinction metrics like [LIFE](https://anil.recoil.org/projects/life) ([paper](https://anil.recoil.org/papers/2024-life)) 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](https://anil.recoil.org/ideas/tessera-habitat-maps) 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"](https://anil.recoil.org/ideas/tessera-interpretable-downscaling)
is a lot of fun if you want to get into matters of both climate and biodiversity\!
We now know from [Pedro Sousa](https://www.linkedin.com/in/pedro-marques-sousa)'s work that [satellite embeddings improve local forecasting](https://anil.recoil.org/papers/2026-weather-downscaling)
significantly, but [not why](https://anil.recoil.org/notes/weather-downscaling-tessera).
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"](https://anil.recoil.org/ideas/literature-range-habitat-maps)
is one for LLM and VLM aficionados. We're building an agentic pipeline over the millions of conservation fulltexts in [Evidence TAP](https://anil.recoil.org/papers/2025-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"](https://anil.recoil.org/ideas/agentic-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](https://anil.recoil.org/ideas/living-iucn-redlist).
## 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](https://anil.recoil.org/ideas/lean-dijkstra-automata)
(MPhil). Write a cross-layer effect specification once in [Lean 4](https://lean-lang.org) as a Dijkstra
monad, then compile it into proof obligations as well as a runtime automaton in
[OxCaml](https://anil.recoil.org/projects/oxcaml), with a proof that the latter represents the former. I did a much
cruder version of this twenty years ago with [SPL](https://anil.recoil.org/papers/2009-icfem-spl).
Suits someone who wants both proofs and executable fast code.
- [An io\_uring backend for Lean](https://anil.recoil.org/ideas/lean-io-uring-backend) (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](https://anil.recoil.org/notes/icfp25-post-posix) for some background.
- [An antibotty defensive testbed](https://anil.recoil.org/ideas/antibotty-testbed) (MPhil). The time-to-exploit a vulnerability
is [now negative](https://anil.recoil.org/notes/rumour-is-the-exploit). 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](https://mirage.io) 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](https://anil.recoil.org/ideas/tracing-hdl-with-effects)
(MPhil). [HardCaml](https://github.com/janestreet/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](https://github.com/clash-lang/clash-compiler) 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](https://anil.recoil.org/projects/tessera), [Enki](https://anil.recoil.org/projects/enki), [OxCaml](https://anil.recoil.org/projects/oxcaml) or
[Conservation Evidence](https://anil.recoil.org/projects/ce), 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\!
The EEG group last Christmas wearing silly hats, proving we exist. Join usss!
Synopsis: A refreshed set of Part II and MPhil projects, split between environmental science problems that need computer science, and more conventional systems and programming languages topics.
Words: 1224
## Related
- [Celebrating a year of Tessera embeddings and releasing GeoTessera 0.10](https://anil.recoil.org/notes/geotessera-a-year-on) (note, 2026-08-27)
- [Just a rumour of a bug is enough to find a security exploit these days](https://anil.recoil.org/notes/rumour-is-the-exploit) (note, 2026-08-22)
- [Improving local weather forecasts using Tessera embeddings](https://anil.recoil.org/notes/weather-downscaling-tessera) (note, 2026-08-13)
- [Earth observation embeddings are effective sub-grid descriptors for probabilistic weather downscaling](https://anil.recoil.org/papers/2026-weather-downscaling) (paper, 2026-08-01)
- [Can agentic LLMs use local field guides to improve identification of rare species?](https://anil.recoil.org/ideas/agentic-field-guides) (idea, 2026-08-01)
- [An antibotty defensive testbed to protect network services](https://anil.recoil.org/ideas/antibotty-testbed) (idea, 2026-08-01)
- [Compiling Lean specifications into OxCaml enforcement automata](https://anil.recoil.org/ideas/lean-dijkstra-automata) (idea, 2026-08-01)
- [Scanning the literature for species range and habitat maps](https://anil.recoil.org/ideas/literature-range-habitat-maps) (idea, 2026-08-01)
- [Generative detection of ghost roads with Tessera embeddings](https://anil.recoil.org/ideas/tessera-ghost-roads) (idea, 2026-08-01)
- [Global habitat maps from Tessera embeddings](https://anil.recoil.org/ideas/tessera-habitat-maps) (idea, 2026-08-01)
- [Interpretable downscaling of local weather predictions](https://anil.recoil.org/ideas/tessera-interpretable-downscaling) (idea, 2026-08-01)
- [Generating potential natural vegetation maps under contemporary climate with Tessera](https://anil.recoil.org/ideas/tessera-pnv) (idea, 2026-08-01)
- [An io_uring IO implementation for Lean](https://anil.recoil.org/ideas/lean-io-uring-backend) (idea, 2026-04-01)
- [Enki, a Dashboard of Life on Earth](https://anil.recoil.org/projects/enki) (project, 2026-01-01)
- [It's time to go post-POSIX at ICFP/SPLASH 2025](https://anil.recoil.org/notes/icfp25-post-posix) (note, 2025-10-08)
- [AI-assisted Living Evidence Databases for Conservation Science](https://anil.recoil.org/papers/2025-evidence-tap) (paper, 2025-10-01)
- [A Living IUCN Red List of the World's Species](https://anil.recoil.org/ideas/living-iucn-redlist) (idea, 2025-09-01)
- [A hardware description language using OCaml effects](https://anil.recoil.org/ideas/tracing-hdl-with-effects) (idea, 2025-03-01)
- [LIFE: A metric for mapping the impact of land-cover change on global extinctions](https://anil.recoil.org/papers/2024-life) (paper, 2025-01-01)
- [OxCaml Labs](https://anil.recoil.org/projects/oxcaml) (project, 2025-01-01)
- [TESSERA, a pixelwise geospatial foundation model](https://anil.recoil.org/projects/tessera) (project, 2025-01-01)
- [Conservation Evidence Copilots](https://anil.recoil.org/projects/ce) (project, 2024-01-01)
- [Mapping LIFE on Earth](https://anil.recoil.org/projects/life) (project, 2023-01-01)
- [Planetary Computing](https://anil.recoil.org/projects/plancomp) (project, 2022-01-01)
- [Unikernels](https://anil.recoil.org/projects/unikernels) (project, 2010-01-01)
- [Combining Static Model Checking with Dynamic Enforcement Using the Statecall Policy Language](https://anil.recoil.org/papers/2009-icfem-spl) (paper, 2009-11-01)
---
Canonical: https://anil.recoil.org/notes/student-projects-2026
Type: note
License: CC BY 4.0
Tags: cambridge, research, teaching, systems
