Como tudo na engenharia de software a resposta é depende rs
Não há bala de prata, como bem disse Brooks, então não há "equivalências", até por que estas práticas/documentos que você citou não são exclusivas a "sistemas".
Além disto, um game é também um software. Então, o que impede um jogo adotar uma ou mais destas práticas? Absolutamente nada.
Você citou diversas práticas em diferentes níveis de abstração, o que torna muito ampla a questão e dificulta uma resposta "exata". Também, por que não é útil um game ter especificação técnica? E por que não padrões de codificação e normas para o projeto? Novamente, nada impede a aplicação de uma ou N práticas da ES no desenvolvimento de games.
Especificamente quanto á sua pergunta:
Qual o equivalente a uma especificação funcional para jogos?
Nada impede ser usado casos de uso, histórias de usuário, modelos de negócio com suas regras, etc.. Porém, devido a algumas especificidades, pode ser que dê bastante trabalho de documentar apenas com práticas mais conhecidas pelo mercado "convencional".
No caso de games existem também práticas bastante aceitas. Um exemplo:
- Game Design Document: com o GDD é possível representar vários aspectos de um game como técnicos (classe e componentes, por exemplo), de design gráfico e também os funcionais, como a história do jogo (como atingir objetivos, por exemplo), seus personagens, etc. Há muita referência e exemplos sobre GDD na web, talvez lhe ajude.
Uma outra consideração quanto a outra pergunta:
Existem ferramentas formais para que se deixe bem claro o objetivo a ser atingido?
Bom, você pode colocar qualquer prática num método formal em ES. Se é sempre funcional e é necessário, aí já são outros quinhentos.
Finalizando e lembrando, não há padrões rígidos na ES, você pode adaptar práticas existentes, compor seu próprio mindset, evoluir conforme suas necessidades e ir sempre além =)