leanviz

Prove a function in Lean 4, call it from C#. lean2il re-checks every proof with Tenet, an independent Lean kernel, compiles the kernel terms to .NET IL, and writes the docs from the Lean. With a VS Code extension.

AES-256 from FIPS-197 in Lean 4: test vectors, decrypt∘encrypt = id, S-box uniformity 4 and nonlinearity 112, branch number 5, ≥25 active S-boxes in any 4 rounds. Kernel-checked, re-checked by Tenet.