Multi-Language Formal Verification/Proof Automation (low latency/realtime applications)
Supported Languages & Formats:
  • C/C++: .cpp, .c, .cc, .cxx, .h, .hpp (C++17 standard)
  • Rust: .rs (Edition 2021)
  • OCaml: .ml, .mli
  • HDL/FPGA: .v, .sv (Verilog/SystemVerilog), .vhd, .vhdl (VHDL)
  • AI/Neural Networks: .onnx, .pb, .pt, .pth, .h5
  • Maximum file size: 5MB
  • Maximum lines of code: 5,000 (not applicable to neural networks)
Upload your source file or model for formal verification
Maximum allowed notional value
Maximum orders per second
Maximum data age before kill-switch
Verification Process
1. Code Analysis
Clang → LLVM → CBMC
2. Model Checking
Bounded verification with Z3
3. Proof Generation
DRAT proofs & audit artifacts
Offline Artifact Verification

Upload previously generated verification artifacts for independent validation:

Upload .tar.gz artifact bundle for verification