Generated Verified, Valid Faithful: Why I’m Building Protocol 17

Elon landau — Tue, 11 Aug 2026 13:23:03 +0000

Protocol 17

I’ve been building an experimental open-source project called Protocol 17.

It started from a simple frustration I had with AI-assisted coding:

If I explicitly write something, why should the model be allowed to silently rewrite it?

A loop boundary, a variable name, an intermediate operation, or a piece of data flow may look like an implementation detail to an LLM — but it may be something the programmer deliberately chose.

So Protocol 17 is based on one rule:

What the programmer explicitly writes is a constraint.
What they leave unspecified is implementation freedom for the AI.

Or, more simply:

AI can fill the blanks. It cannot take the pen.

What does P17 look like?

A Protocol 17 source file can mix natural language, mathematical notation, familiar programming syntax, and native code.

For example:

int a,b
input(a,b)
输出(a+b)

The model may translate this into C:

include

int main(void) {
int a, b;
scanf("%d %d", &a, &b);
printf("%d\n", a + b);
return 0;
}

Or Python:

a = int(input())
b = int(input())
print(a + b)

The programmer specified the variables, input, operation, and output.

The model fills in the target-language implementation.

Generated ≠ Verified

While testing Protocol 17 with a local Qwen 4B model, I got Rust code similar to this:

let mut n: i32 = 0;
std::io::stdin().read_line(&mut n).unwrap();
n = n.trim().parse::().unwrap();

It looks plausible at first glance.

But it is invalid Rust.

read_line expects a mutable String, not an i32, and .trim() is not defined on an integer.

That led me to separate generation from verification:

P17 source
↓
user-selected model
↓
generated target code
↓
gcc / rustc / Python compile()
↓
PASS / FAILED

Protocol 17 currently performs deterministic target verification:

C17 → gcc -std=c17 -fsyntax-only
Python → compile(..., "exec")
Rust → rustc --emit=metadata

The important idea is:

A model returning code does not mean the code has been verified.

But compilation only catches the easy problem

The more interesting problem appeared next.

Suppose the P17 source contains:

for i in 1..n

If .. uses borrowed Rust semantics, the upper bound is excluded.

But a model might translate it into:

for i in 1..=n

That code is perfectly valid Rust.

rustc happily accepts it.

But the model changed something the programmer explicitly wrote.

So:

Valid ≠ faithful.

Another example:

s[i] = p;
cnt[s[i]]++;

A model may notice that s[i] currently equals p and rewrite it as:

s[i] = p;
cnt[p]++;

The result may be equivalent in that particular context.

But it bypasses an explicit intermediate read chosen by the programmer.

Protocol 17 currently treats that as a fidelity violation.

Two different verification problems

I’m therefore thinking about two layers:

Target verification

Is the generated target program legal?

This already exists.

Fidelity verification

Did the generated program preserve the programmer’s explicit constraints?

This does not exist deterministically yet.

And I think the second problem is much more interesting.

Bring Your Own Model

Protocol 17 is not tied to one AI provider.

The current alpha supports a provider layer for OpenAI-compatible APIs, Anthropic, Gemini, and local OpenAI-compatible servers such as Ollama.

So the architecture is roughly:

            Protocol 17
                 │
          Provider adapter
                 │
   ┌─────────────┼─────────────┐
   ↓             ↓             ↓

OpenAI-compatible Anthropic Gemini
│
└── local Ollama / other compatible models

The model is replaceable.

The protocol and verification layers are the part I want to keep stable.

Current state

Protocol 17 is still an experimental alpha.

Right now it has C17, Python, and Rust translation; deterministic target verification; a VS Code prototype; reverse code explanation; BYOK/BYOM support; and local-model support.

There is no formal parser, AST, or IR yet, and deterministic fidelity verification is still an open problem.

I’m deliberately building small pieces first rather than pretending the protocol is already formally defined.

The next major milestone is figuring out how much of fidelity verification can be made deterministic without turning P17 into another rigid programming language.

GitHub:

https://github.com/epsilon-lain/Protocol-17

I’d be very interested in criticism, related work, or ideas about the distinction between validity and fidelity in AI-generated code.

DEV Community: Elon landau

Generated Verified, Valid Faithful: Why I’m Building Protocol 17

include