Ada

为零容忍故障而设计

1970年代，美国国防部面临的问题是：军事软件使用数百种不兼容语言，代码质量参差不齐，维护成本极高。DoD发起竞标设计新语言，最终选择了Jean Ichbiah团队的方案，命名为Ada（纪念世界首位程序员Ada Lovelace），1983年成为军事采购的强制标准。

Ada的安全特性渗透到语言每个角落：子类型（Subtype）可以限制值的范围（如type Day is range 1..31），越界在运行时抛出异常；数组索引从任意值开始，消灭了「差一」错误；参数方向（in/out/in out）让函数接口的读写意图明确；任务（Task）是语言级别的并发单元，带有受保护对象（Protected Object）的互斥访问。[1]

SPARK与形式验证

SPARK是Ada的一个子集，配套工具链可以对代码做形式验证（数学证明程序满足规约，而不只是测试）。通过添加合约（前置条件、后置条件、不变量）作为注解，SPARK的证明器可以静态验证：数组不越界、没有整数溢出、逻辑前提总是满足。

空客A380的部分飞控代码、伦敦地铁的CBTC系统（无人驾驶控制）使用Ada/SPARK，安全级别达到DO-178C最高级（DAL A）。AdaCore公司维护GNAT编译器和SPARK工具链，面向航空、铁路、汽车（ISO 26262）市场。在「软件缺陷可能导致人员伤亡」的场景，Ada/SPARK提供的可验证安全性是其他主流语言难以企及的。