DEV Community: Gowri shankar

Your verifier is probably lying to you about floats

Gowri shankar — Tue, 18 Aug 2026 12:23:31 +0000

Here is a promise that looks obviously true:

fn add_twice(x: Float) -> Float
    ensures result == x + 0.2
{
    return x + 0.1 + 0.1
}

Adding a tenth twice is the same as adding two tenths. Every algebra teacher you have ever had agrees. Most program verifiers agree too.

They are wrong, and so is the promise.

Velaris — a language I have been building — refuses to prove it, and hands back the number that breaks it:

error[E700] promise cannot be kept: 'add_twice' ensures result == x + 0.2
  proven without running the program:
    x = -1.207290298954004637010939404717646539211273193359375
    gives result = -1.007290298954004459375255464692600071430206298828125

That is not a rounding display artifact. Those are two different doubles, and the program really does produce the second one.

Why the lie is tempting

To prove things about numbers, a verifier translates your code into formulas for a solver. The question is which theory to translate into.

The comfortable choice is the theory of real numbers. Reals are associative, commutative, infinitely precise, and solvers are fast at them. Translate Float to Real and everything works beautifully: proofs come back in milliseconds, and x + 0.1 + 0.1 == x + 0.2 is trivially true.

It is also a statement about a machine that does not exist.

Your processor implements IEEE-754 binary64. In that world 0.1 is not one tenth — it is the nearest double to one tenth, which is 0.1000000000000000055511151231257827021181583404541015625. Every operation rounds to the nearest representable value. Addition is not associative. Adding a tenth twice takes two rounding steps; adding two tenths takes one. For many values of x those disagree in the last bit, and one bit is all it takes for == to be false.

So a verifier that models floats as reals will happily certify code that fails on the machine it is compiled for. The proof is valid. The theorem is about the wrong object.

What honesty costs

Z3 has a floating-point theory that implements IEEE-754 exactly: rounding modes, subnormals, infinities, NaN, signed zero. Velaris translates Float into that theory rather than into Real.

The bill arrives immediately.

It is slow. The FP theory is decided by bit-blasting — expanding 64-bit values into circuits of individual bits and handing the result to a SAT solver. The refutation above takes about fifteen seconds. Integer proofs in the same compiler finish in milliseconds.

Fewer things are provable. Plenty of true-in-the-reals facts are simply false in IEEE-754, and plenty of true-in-IEEE facts are too expensive to establish. A verifier that pretends floats are reals has a much better success rate on paper. It is winning a game nobody should want to play.

Equality gets strange, correctly. Velaris compares floats with fpEQ, not structural equality, which means NaN is not equal to itself and positive zero equals negative zero. Both are IEEE behaviour, and both surprise people. Using structural equality would have been faster and easier to explain, and would have quietly produced false results at the edges.

There is a bonus that only shows up once you are honest: comparison constraints start doing real work. A precondition like requires x >= 0.0 silently rules out NaN, because NaN fails every comparison. The prover knows that, so a promise you could not otherwise establish sometimes becomes provable for free.

The rule underneath

Velaris has one commitment it will not trade away: it never claims something is proven unless the claim is literally true.

That single rule decided the float design by itself. If you model floats as reals, "proven" starts meaning "proven about an idealised machine that does not exist," and the word has quietly been devalued. Everything after that is negotiation.

The same rule shows up elsewhere in the compiler. Division and modulo are not native-compiled, because a native fdiv by zero yields infinity while the language promises a clean error, and two execution modes that disagree are worse than one slow mode. A premise the solver cannot translate aborts the whole proof rather than being silently dropped, because proving with dropped premises manufactures false counterexamples. Anything unprovable degrades to a runtime check rather than being waved through.

None of these make the demo look better. All of them are the reason the demo can be believed.

Try it

The compiler runs in your browser, no install: the Velaris playground

Paste the function from the top of this post and watch it refuse. Then change ensures result == x + 0.2 to something IEEE actually guarantees — say ensures result >= x — and watch it go through.

Or install it:

pip install velaris-lang

If you can make Velaris say "proven" about something that is false at runtime, that is a soundness bug, and this project treats those as security reports.

github.com/gowrishankar-infra/velaris-lang

Velaris is a language where a function's signature declares its types, the effects it may perform, whether it can fail, and promises checked by Z3 before the program runs. Built with heavy AI assistance across 80+ releases; the design decisions were mine and the commit history is the honest record.

I built a local AI coding system that actually understands your codebase — here's what I learned

Gowri shankar — Fri, 10 Apr 2026 02:07:48 +0000

I'm Gowri Shankar, a DevOps engineer from Hyderabad. I just open-sourced a project I've been building for the past few weeks, and I want to share it honestly — what it does, how I built it, and what I learned.
🔗 GitHub: github.com/gowrishankar-infra/leanai

🤔 The Problem
Every AI coding tool I've used has the same frustration: it sees my code for the first time, every time.
I paste a snippet, explain the context, get an answer, close the tab — and next session, start from zero. Claude doesn't know my project structure. GPT doesn't remember what we discussed yesterday. Copilot suggests function names that don't exist in my codebase.
I wanted an AI that permanently understands my project. So I built one.

🧠 What LeanAI Does
LeanAI is a fully local AI coding assistant. It runs Qwen2.5 Coder (7B and 32B) on your machine. No cloud, no API keys, no subscriptions, no data leaving your computer.
Here's what makes it different from existing tools:
📂 It knows your entire codebase
Run /brain . and LeanAI scans your project with full AST analysis:
[Brain] Scanned 91 files in 5674ms
Functions: 1,689
Classes: 320
Dependency edges: 9,775
When I ask "what does the engine file do?", it describes MY actual engine with MY real classes — not a generic example about what an engine file might look like.
⚡ Sub-2ms autocomplete from your project
Type /complete gen and in 0.8ms, it returns completions from YOUR codebase:
◆ GenerationConfig core/engine.py
ƒ generate() core/engine_v3.py
ƒ generate_changelog() brain/git_intel.py
ƒ generate_batch() core/engine_v3.py
No model call needed. It searches the brain's index of 2,899 functions directly.
🔍 Semantic git bisect

This one doesn't exist anywhere else.

Instead of binary search for bugs, LeanAI reads each commit semantically and predicts which one introduced a bug:
/bisect authentication stopped working

Most likely culprit:
b7b3f51 — VS Code extension + path separator fix
Suspicion: 45%
Reasoning: includes path changes that could affect auth flow
It analyzed 20 commits, scored each one, and explained its reasoning.
🛡️ Adversarial code verification
Instead of just running tests, LeanAI generates edge-case inputs designed to break your code:
/fuzz def sort(arr): return sorted(arr)

Tested: 12 | Passed: 9 | Failed: 3

Failures:
✗ None → TypeError
✗ [1, 'a', 2.0] → TypeError
✗ [1, None, 3] → TypeError

Suggested fixes:
→ Add None check
→ Add type validation
Found 3 bugs in under 1 second.
💾 It never forgets
Every conversation is stored in persistent session memory. Session 1's decisions are searchable in session 10. It tracks how your understanding evolves across sessions — from "setting up a database" to "optimizing cache invalidation" — and predicts what you'll need next.
📈 It gets smarter from your code
Every interaction auto-collects training data. When you have enough examples, QLoRA fine-tuning makes the model learn YOUR coding patterns. No other tool does this.

🤝 The Honest Part
I built this using Claude. Claude wrote most of the code. I made every architectural decision, debugged every Windows/CUDA issue, tested everything on my machine, and directed every phase of development.
I think this is how software gets built in 2026. 92% of developers use AI coding tools. The value isn't in typing code — it's in knowing what to build, how to architect it, and when something is wrong. I'm not hiding Claude's involvement because I don't think it diminishes the work.

⚠️ What It's NOT
I want to be upfront about the limitations:
LimitationDetails🐢 It's slow25-90 seconds per response on CPU. Cloud AI gives you 2-5 seconds.🧠 Not as smart as GPT-4/ClaudeNever will be at this model size. The value is project awareness.🔧 It's roughThis is v1. There are bugs. The UI is basic.

📊 The Numbers
MetricValueIntegrated systems29Tests (all passing)500+Lines of Python27,000+CLI commands45+API endpoints32Interfaces3 (CLI, Web UI, VS Code)Models2 (7B fast, 32B quality)Monthly cost$0

🏆 Features No Competitor Has
I searched the internet and compared with every major open-source AI coding tool — Aider (39K stars), Continue (20K stars), Tabby (20K stars), Forge, OpenClaw (70K stars). None of them have ALL of these:

FeatureUnique?1Sub-2ms autocomplete from AST brain index✅2Semantic git bisect with AI suspicion scoring✅3Adversarial code fuzzing with fix suggestions✅4Cross-session evolution tracking✅5Predictive pre-generation✅6Continuous fine-tuning pipeline✅7Full AST dependency graph (9,775 edges)✅8TDD auto-fix loop✅93-pass reasoning engine✅104-pass writing engine✅11Multi-model auto-switching by complexity✅
Individual features exist in other tools. Nobody has integrated them all in one offline system.

🛠️ Tech Stack
Models: Qwen2.5 Coder 7B + 32B (GGUF, via llama-cpp-python)
Memory: ChromaDB + sentence-transformers
Server: FastAPI + uvicorn
Brain: Custom AST parser with dependency graph
Language: Python
License: AGPL-3.0
Hardware: i7-11800H, 32GB RAM, RTX 3050 Ti

💡 What I Learned

AI is a coding partner, not a replacement. Claude wrote the code, but it couldn't have built LeanAI without me deciding what to build, in what order, and catching when things broke.
Local AI is viable on consumer hardware. My laptop runs a 32B parameter model. It's slow, but it works. When Qwen3 and Llama 4 drop, the infrastructure I built is ready.
Project awareness is an unsolved problem. Every AI tool treats your codebase as a stranger. Building a "brain" that maps functions, tracks dependencies, and remembers conversations is the hard part — not the model inference.
Testing everything matters. 500+ tests across 18 files. Every system tested independently. This saved me dozens of times when one change broke something else.

🚀 Try It
bashgit clone https://github.com/gowrishankar-infra/leanai.git
cd leanai
pip install -r requirements.txt
python main.py
Then run /brain . to scan your project and start asking questions.
🔗 GitHub: github.com/gowrishankar-infra/leanai
⭐ Star it if you think local AI that understands your codebase is worth building.

UPDATE: Qwen3-Coder-30B Now Running Locally (April 2026)

Since the original post, LeanAI has shipped major upgrades:

Qwen3-Coder-30B-A3B — response times went from 5-7
minutes to ~2 minutes on the same hardware. Mixture-of-Experts
architecture: 30B total params, only 3B active per token.

6 novel features no cloud AI has:

Code-Grounded Verification (fact-checks AI claims against your AST)
Cascade Inference (7B drafts → 32B reviews, 3x faster)
Mixture of Agents (multi-perspective code reviews)
ReAct (model looks up real code before answering)
Multi-language brain (20+ language parsers)
KV Cache optimization (15-25% faster)

Now at 40 technologies, 31,000 lines, 99 files.

I'd love feedback, bug reports, or honest criticism. I know it's not perfect — that's why I'm sharing it.
— Gowri Shankar

What I shipped this week on khaga.dev — Fix It buttons, health scores, and 24/7 alerts

Gowri shankar — Mon, 16 Mar 2026 13:46:49 +0000

What I shipped this week on khaga.dev — Fix It buttons, health scores, and 24/7 alerts

Two weeks ago I launched khaga.dev — a free AI tool that diagnoses AWS, GCP, Azure, and Kubernetes infrastructure in seconds using Claude AI.

This week I shipped 5 major features based on early feedback. Here's what's new.

⚡ Fix It button

The most requested feature. Every finding now has a Fix It button.

Click it and you get:

The exact shell command to fix the issue
A context-aware safety checklist (different for kubectl vs aws vs terraform)
One-click copy to clipboard
"Copy & Open Remediate" to run it directly in Khaga

Example for a CRITICAL finding on a Dockerfile:

Fix: sed -i 's/FROM ubuntu:latest/FROM ubuntu:22.04/' Dockerfile

No more Googling at 2am.

📊 Infrastructure Health Score

The dashboard now shows a 0-100 health score per cloud provider on login.

🟢 70-100 = Healthy
🟡 40-69 = Degraded
🔴 0-39 = Critical

Scored based on the severity and frequency of findings across your last 500 diagnoses. Click any score card to jump straight to that provider's diagnosis.

🌍 Multi-region AWS scan

Previously Khaga only scanned one AWS region. Most people have resources spread across multiple regions and were missing issues.

Now there's a "Scan all regions" checkbox on the AWS panel. Check it and Khaga scans all 6 major regions in parallel:

us-east-1, us-west-2, eu-west-1, ap-south-1, ap-southeast-1, ap-northeast-1

All findings get tagged with their region.

🔔 24/7 Automated Alerts

Khaga now runs in the background and alerts you when critical issues are detected — without you having to manually trigger a diagnosis.

Set your scan frequency in Settings:

Disabled
Every hour
Daily
Weekly

Alerts arrive via Slack (Block Kit formatted) or email (HTML template via Resend) with a "View in Khaga" button.

⚡ Streaming responses

Predictive analysis and Compliance used to show a spinner for 20-30 seconds. Users were abandoning before results loaded.

Now results stream in — the UI shows an animated progress indicator within 1-2 seconds and snaps to the final result when done.

What's next

GitHub Actions integration (scan on every deploy)
Slack bot (/khaga scan aws)
Team accounts

All of this is free at khaga.dev. No credit card, no setup beyond adding your cloud credentials.

If you run AWS/K8s/GCP without a dedicated SRE team — this is built for you.

What feature would make you actually use this daily? Drop it in the comments.

Built with Flask, PostgreSQL, Claude AI (Anthropic), deployed on Railway.

#devops #aws #kubernetes #showdev #webdev

I built a free AI tool that diagnoses AWS/Kubernetes infrastructure in seconds

Gowri shankar — Thu, 05 Mar 2026 13:56:01 +0000

I got tired of the same thing every DevOps engineer knows too well — something breaks in prod, alerts fire, and you spend the next 3 hours jumping between CloudWatch, kubectl logs, Azure Monitor, and 4 other dashboards trying to figure out what actually happened.
So I built Khaga.
You point it at your AWS, GCP, Azure, or Kubernetes setup and it gives you root cause analysis in plain English — what broke, why it broke, and the exact commands to fix it. No more guessing, no more tab switching.
It also does:

Terraform plan security review
Dockerfile analysis
CI/CD log parsing
Helm chart review
SOC2 and ISO27001 compliance estimates
Predictive diagnosis — what's likely to break next
Cross-cloud correlation across all providers simultaneously

The compliance feature is something I'm particularly proud of. SOC2 assessments are normally out of reach for small teams. Khaga gives you a preliminary assessment free with honest AI disclaimers — it tells you what it can't assess, not just what looks good.
Everything is free right now at khaga.dev.
just sign in with Google.
I'd genuinely love feedback from people who manage infrastructure day to day. What's missing? What would make this actually useful in your workflow?
Built with Flask, Claude AI, PostgreSQL. Happy to answer questions about the architecture in the comments.