Bornat's research interests includes program proving in separation logic.
In 2004, one of Bornat's students developed an aptitude test to "divide people up into programmers and non-programmers before they ever come into contact with programming."