可以證明的軟體。
我們把您現有的軟體移轉到 SPARK Ada，並加以證明：證明器能表述的每一項性質，都會針對所有輸入逐一檢查；尚未證明的，會明確告訴您。
- queue
- forge
- prove
- admit
- deliver
PROVEN
示意圖：每個建置都會經過的階段——並非真實的工作。
經過證明，而非抽樣
測試只檢查有人想到要寫的路徑。證明涵蓋型別允許的每一個輸入，我們也會讓您看到哪些檢查通過、哪些沒有。
密封交件（即將推出）
我們正在打造一種方式：讓您在程式碼離開您手中之前，先用專為您發行的金鑰密封，除非您要求，這裡沒有人能閱讀。此功能尚未開放；開放之前，傳送程式碼前請先與我們聯絡。
從倫敦到臺北
我們以英文和繁體中文服務，協助想要汰換已無法擔保之軟體的機構。
本公司出品：Crucible，我們的證明工具——以 AGPL 授權開源，亦提供商業授權；以及 Ghillie，在您自己電腦上執行的小助手。