My advice to those who would like to compete with SPARK is: get at least some people in the team excited about the static analysis part of the project, and some people excited about the embedded development part of the project. That has been a successful combination for our own little projects at AdaCore, like the Tetris or the train demo. Of course, some people can do both but in any case some people in the team (not necessarily the same people) have to be excited by both parts.
In the SPARK team, we'll be happy to help those who would like to compete with part of their Ada code in SPARK. You can ask us questions on the public mailing-list or in the chatroom for the competition.
The website for the competition is here.