Is anyone developing anything like a Debian GNU/hurd/seL4 ?

Tesseractic writes: Is there any such thing as Debian GNU/hurd/seL4 or similar?
If so, I want in on it.
If not, I want to start a project to develop it.
I am NOT currently a debian developer, but I will join if it gets developer support.

The seL4 bit implies use of the seL4 microkernel instead of the Mach microkernel. seL4 is mathematically verifiable by running an automatic proof generator and (a) checker. There are several variants, including several of the Raspberry Pis in addition to at least one other single board computer that is verified down to the metal. I think there's an amd64 version. seL4 is Open Source, of course, or I wouldn't suggest it. The USA used it for some weapon systems. There are some hard real-time versions, which makes it especially useful for that, and which makes using it as a controller of things like stepper motors and servo motors and other devices much less problematic in what passes for the real world in this vicinity. Be warned that the specification language is likely to be unfamiliar to you, so it requires a different, but in my opinion valuable, skill set. Anyone interested? Ask questions in the comments and I'll try and answer them. Someone call Stallman for me. I have some advice for him and I'd like it if he would participate. There's also a related concept called TrustWorthy which you can google. Basically, the _owner_ can trust the device.