Hacker News

Show HN: OxiLean – Pure Rust Interactive Theorem Prover (Zero C Deps, WASM)

Hacker News - Fri, 03/06/2026 - 6:04am

Hey HN,

Just dropped v0.1.0 of OxiLean yesterday.

It's a full Interactive Theorem Prover written 100% in Rust (1.2 million lines across 11 crates). Inspired by Lean 4, implements Calculus of Inductive Constructions, universe polymorphism, dependent types, full tactic framework (intro/apply/simp/ring/omega etc.), and even LCNF-based codegen.

Key points that actually matter: - Kernel has literally zero external crates and zero unsafe. Memory-safe by design, no unwraps, explicit errors everywhere. - Runs in the browser via WASM (npm package @cooljapan/oxilean ready). - REPL works out of the box: cargo run --bin oxilean - No C/Fortran anywhere — unlike original Lean.

Repo: https://github.com/cool-japan/oxilean

WASM demo snippet in README if you want to play instantly.

On my machine I've already proven 99.24% of MathLib4's 179,668 declarations (aiming for 100% in 0.1.1 soon). Been grinding this because I got tired of C++/OCaml build hell in formal methods tools.

Curious what you think — especially if you're into formal verification in Rust or using Lean.

Comments URL: https://news.ycombinator.com/item?id=47273461

Points: 1

# Comments: 0

Categories: Hacker News

Show HN: Markdown-to-Book – Convert Markdown to KDP Ready PDFs and EPUBs

Hacker News - Fri, 03/06/2026 - 6:02am

Author here. I'm a software engineer who started writing hard science fiction on the side. I built this tool because I wanted to write in plain Markdown and go straight to Amazon KDP without touching Word, InDesign, or Vellum.

The workflow: I write stories in .md files, one heading per chapter, --- for scene breaks. When I'm ready to publish, I run one command and get a paperback PDF, hardcover PDF, and Kindle EPUB with correct margins, typography, and scene breaks. The tool wraps Pandoc and XeLaTeX with a custom LaTeX template and a Lua filter that handles the scene break conversion. Commander.js is the only Node dependency.

I used this to publish my first novelette, a hard sci-fi story called "The Pull" about an astrophysicist mapping the Zone of Avoidance behind the Milky Way. The science in the story is grounded in real astrophysics (the Great Attractor, large scale cosmic flows, the Zone of Avoidance). I also built an author website at 'alanvoss.me' with Next.js and Payload CMS, deployed as a static site on Vercel, where you can read the first chapter and see the characters.

On AI use and Graphics: The story concept and science are mine. I used Claude Opus 4.6 to help with some character dialogue and for grammar and spelling checks. Character portraits on the website were generated with Midjourney and OpenAI image models. Book covers were made in Canva.

The tool itself is simple (~200 lines of JS), but it solved a real problem for me. The KDP margin requirements are fiddly, especially the difference between paperback and hardcover inner margins, and getting scene breaks to render correctly in both LaTeX and EPUB needed the Lua filter approach. Hopefully useful to other developers who write.

Please let me know if you have any questions about the tool, the publishing process, or KDP in general.

Comments URL: https://news.ycombinator.com/item?id=47273448

Points: 1

# Comments: 0

Categories: Hacker News

Malicious NPM package pino-SDK-v2 exfiltrates .env secrets to Discord

Hacker News - Fri, 03/06/2026 - 5:57am

We just analyzed a fresh supply chain attack on npm that's pretty well-executed.

Package: pino-sdk-v2 Target: Impersonates pino (one of the most popular Node.js loggers, ~20M weekly downloads)

Reported to OSV too- https://osv.dev/vulnerability/MAL-2026-1259

What makes this one interesting: The attacker copied the entire pino source tree, kept the real author's name (Matteo Collina) in package.json, mirrored the README, docs, repository URL so everything looks legitimate on the npm page.

The only changes: - Renamed package to pino-sdk-v2 - Injected obfuscated code into lib/tools.js (300+ line file) - No install hooks whatsoever

The payload: Scans for .env, .env.local, .env.production, .env.development, .env.example files, extracts anything matching PRIVATE_KEY, SECRET_KEY, API_KEY, ACCESS_KEY, SECRET, or just KEY=, then POSTs it all to a Discord webhook as a formatted embed.

The malicious function is literally named log(). In a logging library. That's some next-level camouflage.

Why most scanners miss it: - No preinstall/postinstall hooks (most scanners focus on these) - Executes on require(), not during install - Obfuscated with hex variable names and string array rotation

Trusted metadata makes the npm page look legit

If you've installed it:

Remove immediately and rotate all secrets in your .env files. Treat it as full credential compromise.

Full technical analysis with deobfuscated payload and IOCs: https://safedep.io/malicious-npm-package-pino-sdk-v2-env-exfiltration/

Comments URL: https://news.ycombinator.com/item?id=47273407

Points: 1

# Comments: 0

Categories: Hacker News

Last Year of Terraform

Hacker News - Fri, 03/06/2026 - 5:55am
Categories: Hacker News

Show HN: Evalcraft – cassette-based testing for AI agents (pytest, $0/run)

Hacker News - Fri, 03/06/2026 - 5:52am

Testing AI agents is painful. Every test run calls the LLM API, costs real money, takes minutes, and gives different results each time. CI? Forget about it.

Evalcraft fixes this with cassette-based capture and replay — think VCR for HTTP, but for LLM calls and tool use.

How it works:

1. Run your agent once with real API calls. Evalcraft records every LLM request, tool call, and response into a JSON cassette file.

2. In tests, replay from the cassette. Zero API calls, zero cost, deterministic output.

3. Assert on what matters: tool call sequences, output content, cost budgets, token counts.

run = replay("cassettes/support_agent.json") assert_tool_called(run, "lookup_order", with_args={"order_id": "ORD-1042"}) assert_tool_order(run, ["lookup_order", "search_knowledge_base"]) assert_cost_under(run, max_usd=0.01) It's pytest-native — fixtures, markers, CLI flags. Works with OpenAI, Anthropic, LangGraph, CrewAI, AutoGen, and LlamaIndex out of the box. Adapters auto-instrument your agent with zero code changes.

Also ships with golden-set management, regression detection, PII sanitization, and 16 CLI commands for inspecting/diffing cassettes.

555 tests, MIT licensed, `pip install evalcraft`.

Repo: https://github.com/beyhangl/evalcraft PyPI: https://pypi.org/project/evalcraft/ Docs: https://beyhangl.github.io/evalcraft/docs/

Would love feedback from anyone testing agents in CI.

Comments URL: https://news.ycombinator.com/item?id=47273374

Points: 1

# Comments: 0

Categories: Hacker News

Show HN: I built an AI-powered advert – is this the future of advertising?

Hacker News - Fri, 03/06/2026 - 5:04am

I've been thinking about how AI will change advertising. Instead of static banners or landing pages, what if an ad was a conversation? I built a demo to explore this: a fictional luxury EV brand called Vela, with an AI sales consultant named Stella you can actually talk to. Ask her about range, pricing, comparisons to competitors — she knows the product inside out. Try it here: https://99helpers.com/tools/vela-chat The idea is simple: instead of cramming everything into a hero section and hoping someone scrolls, you let the customer ask what they actually care about. The AI handles objections, comparisons, and details on demand. Built with my own platform (99helpers.com) which lets you give an AI chatbot a knowledge base and embed it anywhere. This is one use case I hadn't fully considered until recently — using the chatbot not for support, but as the ad itself. Curious what HN thinks. Is conversational advertising compelling, or just a gimmick?

Comments URL: https://news.ycombinator.com/item?id=47273063

Points: 1

# Comments: 0

Categories: Hacker News

Pages