CryptoLine: Verification of low-level arithmetic assembly
=========================================================

CryptoLine verifies straight-line arithmetic assembly such as bignum multiplication and NTT butterflies, and has been applied to OpenSSL, BoringSSL, wolfSSL and post-quantum NTT implementations.

Maintainer: Academia Sinica (Bow-Yaw Wang)
Website: https://github.com/fmlab-iis/cryptoline
Category: Verified implementations
Targets: Bignum and NTT assembly, OpenSSL, BoringSSL, wolfSSL, PQC NTTs
Approach: Algebraic and range reasoning on straight-line arithmetic code
Access: Open source
Status: Active research
Strengths: Handles large arithmetic kernels. | Applied to production libraries. | Complements SAW-style equivalence.
Limits: Straight-line code only. | Specialist tool. | Academic maintenance.
Firms using it: none listed
Sources: https://github.com/fmlab-iis/cryptoline

Source page: https://sorryfree.com/frameworks/cryptoline/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13