A grand challenge proposal for formal methods: A verified stack

We propose a grand challenge for the formal methods community: build and mechanically verify a practical computing system, from transistors to software. The challenge is both competitive and collaborative. It is collaborative because practical systems are too large for any one group or tool to handle in isolation: groups will have to team together. Furthermore, the vertical integration of systems at different levels of abstractions - from transistors to software - will encourage the team to adopt different tools for different levels and connect them. It is competitive because there are many systems from which to choose and different teams may form around different target systems.