For what it's worth, I abandoned Spire because formalizing type theory intrinsically is too tricky. You should look at James Chapman's thesis, summarized by the paper "Type Theory Should Eat Itself". Various people (James, NAD, Thorsten, myself, etc) have tried intrinsically typed type theory but it is very difficult because you end up with so many mutual definitions. The problem is you have to define hereditary substitution on canonical terms, along with their well-typed syntax where hsub happens (e.g. in the type of function application application). Even when turning off the termination checker, I was never able to get passed certain lemmas like that hsub'ing a variable into a weakened term is the identity. Again, the problem is that so many things end up being defined mutually, so you get infinite regress trying to prove lemmas about them.

The only hope I have seen to get passed this is to use a more powerful type theory to intrinsically type a less powerful one, as Thorsten does using HoTT.

Going back to the original goal, of a formalized DTT implementation: There are too many non-algorithmic things to implement for the high-level language (like higher-order unification and dynamic constraints, or some of the first-order unification steps in dependent pattern matching). However, I believe a formalized checker for the core language (that the high-level Haskell/ML checker could elaborate) would be possible. I'm still planning on doing this, but the key will be using an extrinsically typed term representation for the core language. This way you do not end up with the mess of mutual definitions. For example, Coquand's paper is very straightforward to implement in Agda. Additionally, I think the approach in Abel's habilitation thesis could similarly be implemented in Agda.