architecture

Instruction file imported from Beneficial-AI-Foundation/kani-autopilot-test (.cursor/rules/architecture.mdc). Copyright stays with the author.

The kani autopilot test is a proof of concept for spexus driven workflows.

Background on Spexus

Spexus (the specification transpilation nexus) is a kind of intermediate representation for translating natural language to specifications in a proofstack-agnostic way. So for example, spexus is designed to be able to compile to kani specs as easily as it can compile to refinedc specs.

Spexus code (statics/syntax) looks like this

// Basic arithmetic function
spec divide {
    prec: divisor != 0
    post: result == dividend / divisor
}

// Array operations
spec safe_get {
    prec: index >= 0 && index < len(arr)
    inv: len(arr) > 0
    post: result == arr[index]
}

// Generic function with quantified metavariables
forall T
exists n: n >= 0
spec process_array {
    prec: len(input) == n
    inv: n > 0
    post: len(result) == n
}

// String operations
spec substring {
    prec: start >= 0 && end <= len(text) && start <= end
    post: len(result) == end - start
}

// Simple list processing
spec filter_positive {
    prec: true
    post: forall x in result: x > 0
}

It doesn't have much of a dynamics, but it's semantics are basic hoare logic. So for example, the last entry would correspond to the hoare triple {true} filter_positive {forall x in result: x > 0}

Spexus parsing/syntax checking and translation from spexus to kani is given in the MCP server at nix run github:Beneficial-AI-Foundation/spexus#mcp.

The two features of the kani autopilot test are

1. translation from natural language to spexus
2. synthesis of rust programs that satisfy kani specs that the spexus transpiler gives you