Galois Inc is an awesome company that does difficult R&D, product development, and uses/creates cutting-edge tech. Much of what they do gets put in their GitHub. This paper, which doesn’t have any math or anything, describes general principles they used in their work on high-assurance security of UAV’s for DARPA. Some of the tools, like Ivory and Tower languages, are also open-source.