Overview

Lof is a zero-knowledge circuit programming language designed to eliminate entire classes of vulnerabilities through advanced type system features. Unlike traditional ZK languages where bugs can lead to forged proofs and stolen funds, Lof catches critical errors at compile time.

Why Lof?

Research shows that 90% of ZK circuit vulnerabilities are underconstrained circuits—bugs where the prover can forge valid-looking proofs. Million-dollar exploits have occurred because developers forgot a single constraint or misconfigured a comparison.

Lof prevents these bugs automatically.

Security-First Design

Lof’s type system prevents the most common vulnerabilities found in production ZK circuits:

Underconstrained Circuits (90% of bugs)

This creates a vulnerability:

proof BadExample {
    witness x: field;
    witness y: field;
    
    assert y === 42  // ERROR: x is unconstrained
}

Lof catches this:

Error: Unconstrained witness 'x'
  --> proof BadExample:2
  |
2 |     witness x: field;
  |             ^ this witness must appear in at least one constraint
  |
  = All witnesses must be constrained to prevent forged proofs

What Lof prevents:

  • Witnesses that don’t affect circuit outputs
  • Forged proofs from malicious provers
  • Missing constraints on critical values

Division by Zero (20+ known exploits)

Dangerous code:

proof UnsafeDivision {
    witness x: field;
    witness y: field;
    witness result: field;
    
    assert result === x / y  // ERROR: y not proven non-zero
}

Lof catches this:

Error: Potential division by zero
  --> proof UnsafeDivision:5
  |
5 |     result === x / y
  |                    ^ divisor 'y' not proven to be non-zero
  |
  = Add constraint: assert y != 0

Non-Binary Boolean Values (Found in conditional logic)

proof BadSelector {
    witness selector: field;  // Intended to be 0 or 1
    input a: field;
    input b: field;
    output result: field;
    
    result === selector * a + (1 - selector) * b
    // Malicious prover can set selector = 0.5!
}

Lof enforces binary constraints automatically:

proof SecureSelector {
    witness selector: bool;  // Lof generates: selector * (1 - selector) === 0
    input a: field;
    input b: field;
    witness result: field;
    
    assert result === selector * a + (1 - selector) * b
}

Field Overflow in Comparisons

proof BadRangeCheck {
    witness value: field;
    output is_small: bool;
    
    is_small === value < 100
    // Lof generates proper range-check constraints:
    // 1. Bit-decomposition of value
    // 2. Bounded comparison logic
    // 3. Boolean constraint on result
}

Example: Complete Secure Circuit

proof SecureAuthentication {
    // Private input
    witness secret_key: field;
    
    // Public inputs
    input commitment: field;
    input challenge: field;
    
    // Public output
    output is_valid: bool;
    
    // Lof ensures:
    // 1. secret_key is constrained (appears in hash)
    // 2. is_valid is a real boolean (0 or 1)
    // 3. All arithmetic is sound
    
    let hash_output = hash(secret_key);
    assert hash_output === commitment;
    
    let response = secret_key + challenge;
    is_valid === response != 0
}

Get Started

Build secure ZK circuits with confidence: