It was actually about 28 py, but that number would come down to 10 if they were to do it again.
source: http://ertos.nicta.com.au/research/l4.verified/numbers.pml
source: http://ertos.nicta.com.au/research/l4.verified/numbers.pml
IMHO, these guys are heros merely for undertaking the task, let alone completing it.