There are roughly a million connected devices for every engineer who can secure one.

At the INTERSCT. Conference at TU Eindhoven, Joseph Kiniry gave an invited keynote on what that imbalance means for the systems around us: "Correct-and-Secure-by-Construction, at Machine Speed."

IoT now includes cars, pacemakers, and factory equipment. Failures can cause physical harm. Testing alone cannot establish assurance across an installed base this large.

Security by design has delivered high assurance for decades. Its limiting factor has been cost: precise models, proof engineering, and expert review were affordable mainly in areas such as aerospace and defense.

AI-assisted rigorous engineering is beginning to change that cost.

  • Over nine months, HOARDE, our agent platform for rigorous engineering, moved from line-by-line review of every action to several hundred person-hours of work between human check-ins. That interval grew after thousands of successful, human-gated actions; it was not granted in advance.

  • We built fifteen verified examples across five domains, from parsers and basic ciphers to post-quantum cryptography. The Cryptol integration has required no defect fixes since entering HOARDE.

  • For IKEv2, a protocol used by many VPNs, we linked a symbolic security proof to an executable cryptographic specification. A high-assurance Rust implementation is underway.

  • The same class of tooling can help analyze, retrofit, and update deployed devices, including systems whose original source code is unavailable.

  • HOARDE agents produce machine-checkable evidence, including proofs and provenance, for their actions. Engineers review that evidence rather than relying on a model's confidence.

AI gives us a chance to make rigorous engineering affordable for systems already deployed and for the devices still to come.

Thank you to the NWO INTERSCT program and TU/e for the invitation and the thoughtful discussion.

Visual recap: Correct-and-secure-by-construction, at machine speed (PDF, 8 pages)

If you build or maintain connected devices that have to hold up under scrutiny, we would like to compare approaches. Get in touch.