https://blog.jetbrains.com/ai/2025/11/why-diffusion-models-could-change-developer-workflows-in-2026/

Apparently, some Open-Source (and closed source too, of course) Text/Code Diffusion models are already here. I personally think they are much more prospective for programming than purely autoregressive models.

Unfortunately, at the moment Text Diffusion models perform mostly worse. Which is quite expected as long as they are much more recent invention, and don't yet enjoy years of engineering improvements.

Augmentin

On one hand, it's an ordinary antibiotic. On the other hand, if you're a cyborg with augmenting implants, antibiotics are very likely to be crucial for you due to constant infection concerns.

If you aren't subscribed, Stephen Hancock, one of the main creative forces behind SCP: Overlord, SCP: Dollhouse, and STALKER: Shadow of the Zone, released another excellent SCP short film two days ago:

https://www.youtube.com/watch?v=AXn36jl7dcs

Dear colleagues,

At AWS re:Invent 2025 in Las Vegas, we announced the AWS Nitro Isolation Engine [1, 2, 3], a formally verified enhancement to the AWS Nitro System that enforces isolation between virtual machines hosted on AWS's new Graviton5-based EC2 instances.

Nitro Isolation Engine represents a significant deployment of mechanized proof in production infrastructure, and we therefore wanted to bring this to the attention of the formal methods and programming languages communities. This work builds directly on decades of advances in interactive theorem proving, program verification, and programming languages theory, alongside landmark projects—such as, seL4 [4], CertiKOS [5], SeKVM [6], and many others—that were inspirations for this work.

What is Nitro Isolation Engine?
Nitro Isolation Engine is a small, trusted computing base written in Rust that sits beneath the AWS Nitro Hypervisor, providing a security isolation boundary between the hypervisor and guest virtual machines, and between co-tenanted guest virtual machines. The Nitro Isolation Engine controls the critical hardware features required for isolating customer workloads, primarily control of Stage Two translation tables.

The verification effort
Nitro Isolation Engine was designed with verification in mind from the first line of code. Nitro Isolation Engine is subject to AWS’s existing rigorous engineering practices, including the deployment of property-based-testing and lightweight formal methods, for example the Kani bounded model checker for Rust [7].

Building atop this foundation, we have specified and verified the correctness of Nitro Isolation Engine in Isabelle/HOL [8]. Our model and proofs consist of around 260,000 lines of machine-checked models and proofs. Specifically, we have proved:

Functional correctness: Nitro Isolation Engine behaves as specified for all operations: virtual machine creation, memory mapping, instruction and data abort handling, and so on. As corollaries of our total verification style, we have also proven memory-safety, termination, and absence of runtime errors, providing our modelling assumptions are accurate.
Confidentiality: We prove a noninterference-style property demonstrating the confidentiality of guest virtual machine states, formalized as indistinguishability preservation up-to permitted flows of declassified information out of a guest.
Integrity: The integrity of guest virtual machine state is formalized as a safety property, showing that the private state of one virtual machine is unaffected by operations modifying another distinct virtual machine.
In addition, we have applied Iris [9] and Verus [10] to prove the correctness of the Nitro Isolation Engine’s concurrency primitives, including ticket locks, mutexes, and rendezvous barriers.

For functional verification, we defined μRust, a restricted subset of Rust expressive enough to write Nitro Isolation Engine but amenable to formal reasoning and embedded its semantics into Isabelle/HOL. Specifications are written in separation logic, and proofs proceed via weakest precondition calculus with custom automation. We have made our verification infrastructure open source as the AutoCorrode library [11] for Isabelle/HOL, which may be of independent interest.

Regards,
Automated Reasoning Group, AWS

[1]: https://www.aboutamazon.com/news/aws/aws-graviton-5-cpu-amazon-ec2
[2] : https://www.youtube.com/watch?v=3Gt-30Fm38U https://www.youtube.com/watch?v=3Gt-30Fm38U
[3]: https://www.youtube.com/watch?v=b0P55gHhG4g
[4]: https://sel4.systems/
[5]: https://flint.cs.yale.edu/certikos/
[6]: https://www.usenix.org/conference/usenixsecurity21/presentation/li-shih-wei
[7]: https://github.com/model-checking/kani
[8]: https://isabelle.in.tum.de/
[9]: https://iris-project.org/
[10]: https://github.com/verus-lang/verus
[11]: https://github.com/awslabs/AutoCorrode

https://www.youtube.com/watch?v=CU0VikkaaZ0

Very funny! And pretty exciting too. 😁

https://www.producthunt.com/products/ecosort-2

Potentially useful, but it seems to send your pictures of garbage to Google Gemini. On the other hand, sending garbage to Google Gemini sounds pretty fun even without recycling. 😏

https://openai.com/index/shipping-sora-for-android-with-codex/

Очень умилительный пост. 😊 По итогу OpenAI выяснили, что можно очень быстро написать небольшое приложение с очень высоким уровнем качества, если

— собрать небольшую команду очень квалифицированных инженеров
— не заёбывать их процессами и бюрократией
— тщательно продумать и зафиксировать архитектуру приложения
— на ранней стадии реализовать end-to-end несколько наиболее критичных фич
— методично покрывать всё тестами
— делать (detailed) design review прежде чем кидаться кодить

Это, безусловно, прорыв. Никто до них такого не знал. (Peopleware? Джоэл Спольски? Не, не слышал.)

Для меня загадочными остались только два вопроса:

1. зачем в этой схеме Codex?
2. что ж мешало всем так делать последние ~40 лет?

https://www.youtube.com/watch?v=mQnKZr97y7A

In the essence, it's just a one cool fancy example of probabilistic programming... but it's still cool, though-provoking and kinda deep in more that one way.

https://www.youtube.com/watch?v=D_gs6mTY0w8

A sorta follow-up. Behind the Scenes, a breakdown of the process, the lighting, the props and so on. A must-watch for anyone shooting anything. A lot of tips, tricks and wisdom.

ARMA 5 is already here, you're simply looking in the wrong store! 😂

https://nibblestew.blogspot.com/2023/09/circles-do-not-exist.html

Old news: Circles do not exist... in PDF, apparently. 😁

Случайно купил молотый кофе в такой же пачке, в каких продают зёрна. Пять минут не мог понять, как же его заваривать — кофемолка, очевидно, бесполезна, но с чего тогда начинать, если не с помола?

По итогу оказался вполне неплохой кофе. По крайней мере, пока он свежий. Хотя помол мелковат для воронки, на мой вкус. И много "шелухи" в помоле.

The famous Jeff Dean and Sanjay Ghemawat recently (2025/12/16) updated their quite elaborate and comprehensive article on performance engineering:
https://abseil.io/fast/hints.html

https://youtu.be/aaOZC--KY1w

Konstantin Vasiliev as 2025 draws to the end... 😏

Люблю поздравления от сервисов такси.

С Новым годом, ёпта! Ехай нахуй! Не забудь заказать такси у нас.

Едим салат «Оленье»

За праздники поправился на -500г

Я знаю только то, что ничего не знаю... А большинство не знает и этого.

Т.е. они не знают, что я ничего не знаю, и думают, что я что-то знаю...

Карл Юнг предлагает для канала нативную интеграцию с тенью... 🧐