Albatross 是一门编程语言：
静态验证：可以开发程序和算法，证明在 Albatross 是正确的
证明助手：任意数学理论都可以在 Albatross 表述或者证实
理论证明：包括一个证明引擎
函数式，命令式和并发能力
有其他类似的理论证明：Coq, Isaballe/HOL, PVS, Mizaar, AGDa
