At the High Confidence Software and Systems Conference in Annapolis, Joseph Kiniry gave a talk on autonomous formal methods and the HOARDE platform.

In a nutshell:

  • Forty years of formal methods tools that work, fewer than 5,000 practitioners worldwide. AI now generates code at agent speed while verification still runs at human speed.

  • Autonomous formal methods: AI agents apply formal specification and verification under engineer guidance. The human shifts from writing proofs to setting requirements, reviewing agent output, and gating consequential decisions.

  • HOARDE orchestrates specialized agents, one per discipline, along the NINJA refinement chain, with the right formal tools made accessible to them as typed, auditable calls.

  • We start with cryptography because the bar is high there for a reason. A system that holds up under cryptographic scrutiny holds up downstream, and the work pulls in a variety of formal methods tools that then transfer cleanly to verified implementations all the way down to silicon.

  • Two case studies in flight: a formally verified C=64, an irresistible demo of what smartly orchestrated tool use looks like, with a Cryptol model and a Rust simulator that actually boots; and IKEv2, a protocol that quietly carries an enormous amount of secure traffic and doesn't have a public, mechanized security proof.

  • 25× developer efficiency, engineers learning formal methods in flow on their own systems, and the open-source formal methods ecosystem lifted along with them.

HCSS is rare among technical conferences. Every talk and conversation is substantive, and it remains one of the few rooms where you can pitch a verified C=64 and a verified IKEv2 in the same breath and the audience tracks every detail. We are honored to be a part of it.

Visual recap: Autonomous formal methods at HCSS 2026 (PDF, 8 pages)

If you work on systems where verification is the bottleneck, we would like to compare notes. Get in touch.