Autonomous Formal Methods
ABSTRACT In this talk I will describe HOARDE — the Hierarchical Orchestration of Autonomous Rigorous Digital Entities — built by my company, Sigil Logic, since our founding in September, 2025. HOARDE realizes what we call the NINJA methodology (Non-Intrusive Judicious Assurance): rigorous engineering with applied formal methods, made accessible to every engineering team through AI agents. HOARDE works alongside engineers to autonomously create high-assurance systems, generate formal specifications, find gaps in requirements and design, and prepare artifacts for certification and accreditation. It augments a team with what feels like dozens of coworkers who understand rigorous engineering, model-based development, and formal verification. A critical design constraint is that HOARDE can operate entirely on local models — no cryptographic designs, proprietary specifications, or mission-critical system descriptions are ever sent to cloud-hosted LLMs in a local-only deployment. This privacy-preserving architecture makes HOARDE suitable for sensitive and classified work. HOARDE's agents maintain an unbroken refinement chain — from domain model through requirements, architecture, design, implementation, tests, and formal evidence — with full bidirectional traceability. Every operation produces verifiable evidence with recorded provenance. This is not ad hoc AI-assisted development; it is a principled, reproducible methodology enforced by the agents themselves. While creating rigorous specifications and models, HOARDE also trains engineers in the formal languages and tools working behind the scenes, producing a learning loop that has demonstrated substantial efficiency improvements in our internal case studies and meaningfully up-skills developers as they work. Our flagship application, the Cryptol AI, exposes the Cryptol language and toolchain through high-assurance Model Context Protocol (MCP) servers — typed, schema-validated tool interfaces that constrain agent capabilities and generate auditable evidence. We will use Cryptol AI, running within HOARDE, for a live demo of specification, verification, and property proving. We will discuss how models, specifications, and their relations are organized; how formal methods tools are wrapped with capability safety constraints; which engineering facets have specialized agents; and how evidence chains guarantee that systems have exactly the properties mandated by stakeholder requirements. |
BIO Dr. Kiniry holds a Ph.D. in Computer Science from the California Institute of Technology and brings over 30 years of experience in formal methods, high-assurance systems engineering, cybersecurity, and applied computer science research. He previously served as a Full Professor and Head of the Software Engineering Section at the Technical University of Denmark, held permanent academic positions at four universities across Denmark, Ireland, and The Netherlands, and served as Principal Scientist at Galois, Inc. He is a serial entrepreneur (eight companies) and has secured over $100 million in combined U.S. and European research funding. He has extensive experience on DARPA, NSA, and classified programs, with 100+ peer-reviewed publications. He is now the CEO and Chief Scientist at Sigil Logic and Free & Fair. |